`Compfiles/Imo1993P6.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

62 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1993, Problem 6

There are n > 1 lamps L₀, L₁, ..., Lₙ₋₁ in a circle. We use L_{n+k} to mean L_k. A lamp is at all times either on or off. Initially they are all on. Perform steps s₀, s₁, ... as follows: at step sᵢ, if L_{i-1} is lit, then switch Lᵢ from on to off or vice versa, otherwise do nothing. Show that:

(a) There is a positive integer M(n) such that after M(n) steps all the lamps are on again; (b) If n = 2ᵏ, then we can take M(n) = n² - 1. (c) If n = 2ᵏ + 1, then we can take M(n) = n² - n + 1.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo1993P6.State The state of the system: the on/off states of the lamps (true = on), together with the position of the lamp that may be switched at the next step line 37 source
Source documentation
The state of the system: the on/off states of the lamps (true = on), together with the position of the lamp that may be switched at the next step. Positions are taken modulo n, i.e. in Fin n.

no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin, Bool
```
abbrev State (n : ℕ) := (Fin n → Bool) × Fin n
```
def Imo1993P6.step Documented declaration: step line 42 source
Source documentation
One step of the process, performed at the current position s.2: if lamp s.2 - 1 is on then lamp s.2 is switched, otherwise nothing happens to the lamps; in any case the position advances by one (modulo n).

standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State
Proof uses: Prod.mk, Fin, Bool, Function.update, Prod.fst, Prod.snd, ite, Eq, HSub.hSub, OfNat.ofNat, Bool.true, Bool.not, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.
```
def step {n : ℕ} [NeZero n] (s : State n) : State n :=
…
```
Mentions: Imo1993P6.State
abbrev Imo1993P6.initial The initial state: all lamps on, and the next step happens at lamp 0 line 46 source
Source documentation
The initial state: all lamps on, and the next step happens at lamp 0.

standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State
Proof uses: Prod.mk, Fin, Bool, Bool.true, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
abbrev initial (n : ℕ) [NeZero n] : State n := (fun _ => true, 0)
```
Mentions: Imo1993P6.State
abbrev Imo1993P6.lampsAfter The lamp states after t steps of the process line 49 source
Source documentation
The lamp states after t steps of the process.

standard axioms: propext what this means
Statement uses: Nat, NeZero, Fin, Bool
Proof uses: Prod.fst, Nat.iterate, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial
4 instances, coercions and auxiliary constants left out.
```
abbrev lampsAfter (n : ℕ) [NeZero n] (t : ℕ) : Fin n → Bool :=
…
```
lemma Imo1993P6.toggle_inj For a fixed condition c, the map v ↦ (if c then !v else v) is injective line 55 source
Source documentation
For a fixed condition c, the map v ↦ (if c then !v else v) is injective.

standard axioms: propext what this means
Statement uses: Bool, Function.Injective, ite, Eq, Bool.true, Bool.not
Proof uses: Bool.false, of_eq_true, eq_self, Eq.symm, False.elim, Eq.mp, False, Eq.trans, congr, congrArg, ite_eq_right_of_eq_false, Bool.false_eq_true, Eq.refl, Bool.true_eq_false, ite_eq_left_of_eq_true, Bool.not_false, Bool.not_true
4 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_inj (c : Bool) :
    Function.Injective (fun v : Bool => if c then !v else v) := by
…
```
lemma Imo1993P6.bool_toggle Toggling a lamp according to condition c is xor with c line 61 source
Source documentation
Toggling a lamp according to condition c is xor with c.

standard axioms: propext what this means
Statement uses: Bool, Eq, ite, Bool.true, Bool.not, Bool.xor
Proof uses: Bool.false, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_right_of_eq_false, Bool.false_eq_true, Bool.false_bne, eq_self, Eq.symm, ite_eq_left_of_eq_true, Bool.true_bne, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma bool_toggle (c v : Bool) : (if c then !v else v) = (c ^^ v) := by
…
```
lemma Imo1993P6.step_lamps The lamp component of one step line 65 source
Source documentation
The lamp component of one step.

standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State, Eq, Fin, Bool, Prod.fst, Imo1993P6.step, Function.update, Prod.snd, ite, HSub.hSub, OfNat.ofNat, Bool.true, Bool.not
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
```
lemma step_lamps {n : ℕ} [NeZero n] (s : State n) :
    (step s).1 = Function.update s.1 s.2 (if s.1 (s.2 - 1) then !s.1 s.2 else s.1 s.2) :=
…
```
Mentions: Imo1993P6.State, Imo1993P6.step
lemma Imo1993P6.step_pos The position component of one step line 70 source
Source documentation
The position component of one step.

standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State, Eq, Fin, Prod.snd, Bool, Imo1993P6.step, HAdd.hAdd, OfNat.ofNat
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.
```
lemma step_pos {n : ℕ} [NeZero n] (s : State n) : (step s).2 = s.2 + 1 := rfl
```
Mentions: Imo1993P6.State, Imo1993P6.step
lemma Imo1993P6.pos_after After t steps the position is t (modulo n) line 73 source
Source documentation
After t steps the position is t (modulo n).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Fin, Prod.snd, Bool, Nat.iterate, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial, Fin.NatCast.instNatCast
Proof uses: Nat.recAux, id, OfNat.ofNat, Eq.mpr, congrArg, Fin.natCast_zero, Eq.refl, HAdd.hAdd, Nat.succ, Function.iterate_succ_apply', Imo1993P6.step_pos, Eq.symm, Fin.instAddMonoidWithOne, Nat.cast_add_one
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma pos_after (n : ℕ) [NeZero n] (t : ℕ) :
    (step^[t] (initial n)).2 = ((t : ℕ) : Fin n) := by
…
```
Mentions: Imo1993P6.step, Imo1993P6.initial
lemma Imo1993P6.step_injective The step map is injective: a state has exactly one precursor line 86 source
Source documentation
The step map is injective: a state has exactly one precursor. Indeed, the new position tells us which lamp was just considered, and whether it was toggled is recorded in the (unchanged) previous lamp.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Function.Injective, Imo1993P6.State, Imo1993P6.step
Proof uses: Fin, Bool, Eq, Prod.mk, Function.update, ite, HSub.hSub, Bool.true, Bool.not, HAdd.hAdd, And, Prod.mk.inj, Eq.mp, congr, congrArg, congrFun', Prod, Prod.fst, Prod.snd, ite_congr and 28 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma step_injective {n : ℕ} [NeZero n] (hn : 1 < n) :
    Function.Injective (step : State n → State n) := by
…
```
Mentions: Imo1993P6.step, Imo1993P6.State
lemma Imo1993P6.step_periodic The process is periodic: some positive iterate of step fixes the initial state line 128 source
Source documentation
The process is periodic: some positive iterate of step fixes the initial state. This is because step is an injective (hence bijective) self-map of a finite set, so it has finite order as a permutation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Exists, And, Eq, Imo1993P6.State, Nat.iterate, Imo1993P6.step, Imo1993P6.initial
Proof uses: Function.Injective, Imo1993P6.step_injective, Function.Bijective, Function.Injective.bijective_of_finite, Fin, Bool, Equiv.Perm, Equiv.ofBijective, Exists.intro, orderOf, And.intro, orderOf_pos, HPow.hPow, Eq.mpr, id, congrArg, pow_orderOf_eq_one, Eq.refl, Eq.mp, Equiv.Perm.coe_pow
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma step_periodic (n : ℕ) [NeZero n] (hn : 1 < n) :
    ∃ M : ℕ, 0 < M ∧ step^[M] (initial n) = initial n := by
…
```
Mentions: Imo1993P6.step, Imo1993P6.initial
lemma Imo1993P6.all_on_of_last_only Generic final phase: if after n * (n - 1) steps only the last lamp L_{n-1} is on, then the lamps are turned on one by one and after n² - 1 steps they are all on again line 143 source
Source documentation
Generic final phase: if after n * (n - 1) steps only the last lamp L_{n-1} is on, then the lamps are turned on one by one and after n² - 1 steps they are all on again.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Fin, Eq, Bool, Imo1993P6.lampsAfter, HMul.hMul, HSub.hSub, Decidable.decide, HPow.hPow, Bool.true
Proof uses: Fin.NatCast.instNatCast, Fin.ext, Eq.mpr, HMod.hMod, id, congrArg, Fin.coe_natCast_eq_mod, Nat.mul_mod_right, of_eq_true, eq_self, Prod.fst, Nat.iterate, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial, LE.le, HAdd.hAdd, Or, Nat.recAux, Nat.add_zero and 56 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
```
lemma all_on_of_last_only {n : ℕ} [NeZero n] (hn : 1 < n)
    (h : ∀ i : Fin n, lampsAfter n (n * (n - 1)) i = decide (i.val = n - 1)) :
    ∀ i : Fin n, lampsAfter n (n ^ 2 - 1) i = true := by
…
```
Mentions: h, Imo1993P6.lampsAfter
lemma Imo1993P6.step_lamps_eq_of_pred_off If the lamp checked at a step is off, the step leaves all lamps unchanged line 228 source
Source documentation
If the lamp checked at a step is off, the step leaves all lamps unchanged.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State, Eq, Bool, Prod.fst, Fin, HSub.hSub, Prod.snd, OfNat.ofNat, Bool.false, Imo1993P6.step
Proof uses: Eq.mpr, Function.update, ite, Bool.true, Bool.not, id, congrArg, Imo1993P6.step_lamps, funext, dite, Function.update_self, of_eq_true, Eq.trans, True, congrFun', ite_eq_right_of_eq_false, Bool.false_eq_true, eq_self, Eq.symm, Not and 2 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma step_lamps_eq_of_pred_off {n : ℕ} [NeZero n] {s : State n}
    (h : s.1 (s.2 - 1) = false) : (step s).1 = s.1 := by
…
```
Mentions: Imo1993P6.State, h, Imo1993P6.step
lemma Imo1993P6.step_lamps_toggle If the lamp checked at a step is on, the step flips the current lamp line 239 source
Source documentation
If the lamp checked at a step is on, the step flips the current lamp.

standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo1993P6.State, Eq, Bool, Prod.fst, Fin, HSub.hSub, Prod.snd, OfNat.ofNat, Bool.true, Imo1993P6.step, ite, Bool.not
Proof uses: Eq.mpr, Function.update, id, congrArg, Imo1993P6.step_lamps, dite, Function.update_self, of_eq_true, Eq.trans, True, congr, ite_eq_left_of_eq_true, eq_self, Eq.symm, Not, Function.update_of_ne, ite_eq_right, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma step_lamps_toggle {n : ℕ} [NeZero n] {s : State n}
    (h : s.1 (s.2 - 1) = true) (i : Fin n) :
    (step s).1 i = (if i = s.2 then !s.1 i else s.1 i) := by
…
```
Mentions: Imo1993P6.State, h, Imo1993P6.step
lemma Imo1993P6.all_on_of_lamp1_only Documented declaration: all_on_of_lamp1_only line 252 source
Source documentation
Generic final phase for the n = 2ᵏ + 1 case: if after n * (n - 2) steps only lamp L₁ is on, then after two idle steps the lamps L₂, L₃, …, L_{n-1}, L₀ are turned on one by one, and after n² - n + 1 steps they are all on again.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Fin, Eq, Bool, Imo1993P6.lampsAfter, HMul.hMul, HSub.hSub, Decidable.decide, HAdd.hAdd, HPow.hPow, Bool.true
Proof uses: Prod.fst, Nat.iterate, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial, Fin.NatCast.instNatCast, Fin.ext, Eq.mpr, HMod.hMod, id, congrArg, Fin.coe_natCast_eq_mod, Nat.mul_mod_right, of_eq_true, eq_self, Prod.snd, Bool.false, Imo1993P6.pos_after, Not, propext and 67 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 116 steps
Open to load the checked before-and-after goal states.
```
lemma all_on_of_lamp1_only {n : ℕ} [NeZero n] (hn : 2 < n)
    (h : ∀ i : Fin n, lampsAfter n (n * (n - 2)) i = decide (i.val = 1)) :
    ∀ i : Fin n, lampsAfter n (n ^ 2 - n + 1) i = true := by
…
```
Mentions: h, Imo1993P6.lampsAfter
def Imo1993P6.zstep The same process with lamp values in ZMod 2: toggling is adding the predecessor line 372 source
Source documentation
The same process with lamp values in ZMod 2: toggling is adding the predecessor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Prod, Fin, ZMod, OfNat.ofNat
Proof uses: Prod.mk, Function.update, Prod.fst, Prod.snd, HAdd.hAdd, HSub.hSub
19 instances, coercions and auxiliary constants left out.
```
def zstep {n : ℕ} [NeZero n] (s : (Fin n → ZMod 2) × Fin n) : (Fin n → ZMod 2) × Fin n :=
…
```
def Imo1993P6.zinit line 375 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Prod, Fin, ZMod, OfNat.ofNat
Proof uses: Prod.mk
15 instances, coercions and auxiliary constants left out.
def Imo1993P6.z2b line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Bool
Proof uses: Decidable.decide, Eq
11 instances, coercions and auxiliary constants left out.
lemma Imo1993P6.z2b_one line 379 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Imo1993P6.z2b, OfNat.ofNat, ZMod, Nat, Bool.true
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma Imo1993P6.z2b_zero line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Imo1993P6.z2b, OfNat.ofNat, ZMod, Nat, Bool.false
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma Imo1993P6.z2b_add line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Bool, ite, Imo1993P6.z2b, Bool.true, Bool.not, HAdd.hAdd
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.zadd_self line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.one_add_one_zmod line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ZMod, OfNat.ofNat, Nat, HAdd.hAdd
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.one_add_one_cancel line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, add_assoc, Eq.symm, add_left_comm, Imo1993P6.one_add_one_zmod, add_zero, Eq.refl
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.pos_lemma The position after t steps line 393 source
Source documentation
The position after t steps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Prod.snd, Nat.iterate, Prod, Imo1993P6.zstep, Prod.mk, HAdd.hAdd, Fin.NatCast.instNatCast
Proof uses: LT.lt, NeZero.pos, Nat.recAux, id, of_eq_true, Eq.trans, True, congrArg, Fin.instAddMonoidWithOne, Nat.cast_zero, add_zero, eq_self, Eq.mpr, Nat.succ, Function.iterate_succ_apply', Nat.cast_succ, Eq.symm, add_assoc, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma pos_lemma {n : ℕ} [NeZero n] (x : Fin n → ZMod 2) (p : Fin n) (t : ℕ) :
    (zstep^[t] (x, p)).2 = p + (t : Fin n) := by
…
```
Mentions: Imo1993P6.zstep
lemma Imo1993P6.glue Correspondence between the Bool process and the ZMod 2 process line 406 source
Source documentation
Correspondence between the Bool process and the ZMod 2 process.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Imo1993P6.State, Nat.iterate, Imo1993P6.step, Imo1993P6.initial, Prod.mk, Fin, Bool, Imo1993P6.z2b, Prod.fst, ZMod, OfNat.ofNat, Prod, Imo1993P6.zstep, Imo1993P6.zinit, Prod.snd
Proof uses: Nat.recAux, Prod.ext, funext, Eq.refl, congrArg, Eq.mpr, HAdd.hAdd, id, Nat.succ, Function.iterate_succ_apply', Function.update, ite, HSub.hSub, Bool.true, Bool.not, dite, Function.update_self, Imo1993P6.z2b_add, Eq.symm, Not and 1 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma glue {n : ℕ} [NeZero n] (t : ℕ) :
    (step^[t] (initial n)) =
      (fun i => z2b ((zstep^[t] (zinit n)).1 i), (zstep^[t] (zinit n)).2) := by
…
```
Mentions: Imo1993P6.step, Imo1993P6.initial, Imo1993P6.z2b, Imo1993P6.zstep, Imo1993P6.zinit
def Imo1993P6.lasti The last index of Fin n line 441 source
Source documentation
The last index of Fin n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin
Proof uses: Fin.mk, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def lasti (n : ℕ) [NeZero n] : Fin n := ⟨n - 1, by have := NeZero.pos n; lia⟩
```
lemma Imo1993P6.lasti_val line 443 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Imo1993P6.lasti, HSub.hSub, OfNat.ofNat
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Imo1993P6.zero_sub_one_eq_lasti line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Fin, HSub.hSub, OfNat.ofNat, Imo1993P6.lasti
Proof uses: LT.lt, NeZero.pos, Fin.NatCast.instNatCast, Fin.ext, id, Eq.mpr, HMod.hMod, congrArg, Fin.val_natCast, Nat.mod_eq_of_lt, Eq.refl, HAdd.hAdd, propext, sub_eq_iff_eq_add, Fin.instAddMonoidWithOne, Eq.symm, Nat.cast_add_one, Fin.natCast_self
41 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Imo1993P6.L One full round of the process: L x p = x last + ∑_{i ≤ p} x i in ZMod 2 line 458 source
Source documentation
One full round of the process: L x p = x last + ∑_{i ≤ p} x i in ZMod 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat
Proof uses: HAdd.hAdd, Imo1993P6.lasti, Finset.sum, Finset.range, Fin.mk, HMod.hMod
20 instances, coercions and auxiliary constants left out.
```
def L {n : ℕ} [NeZero n] (x : Fin n → ZMod 2) : Fin n → ZMod 2 :=
…
```
def Imo1993P6.tot Total parity of a lamp vector line 462 source
Source documentation
Total parity of a lamp vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, OfNat.ofNat
Proof uses: Finset.sum, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def tot {n : ℕ} (x : Fin n → ZMod 2) : ZMod 2 := ∑ i, x i
```
def Imo1993P6.eFn The vector with only the last lamp on line 465 source
Source documentation
The vector with only the last lamp on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat
Proof uses: ite, Eq, Imo1993P6.lasti
20 instances, coercions and auxiliary constants left out.
```
def eFn (n : ℕ) [NeZero n] : Fin n → ZMod 2 := fun j => if j = lasti n then 1 else 0
```
Mentions: Imo1993P6.lasti
lemma Imo1993P6.L_apply line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Imo1993P6.L, HAdd.hAdd, Imo1993P6.lasti, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma Imo1993P6.L_add line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Imo1993P6.L, HAdd.hAdd
Proof uses: funext, Eq.mpr, Imo1993P6.lasti, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos, id, congrFun', congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.sum_add_distrib, Mathlib.Tactic.Ring.of_eq, HMul.hMul and 9 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.tot_add line 477 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, OfNat.ofNat, Eq, Imo1993P6.tot, HAdd.hAdd
Proof uses: of_eq_true, Finset.sum, Finset.univ, Eq.trans, True, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.sum_add_distrib, eq_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.tot_eq line 480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Imo1993P6.tot, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos
Proof uses: Finset.univ, Fin.sum_univ_eq_sum_range, Eq.mpr, id, congrArg, Imo1993P6.tot.eq_1, Eq.symm, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.rec, Eq.refl, Fin.ext, Nat.mod_eq_of_lt, Fin.isLt
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.eFn_lasti line 489 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, ZMod, OfNat.ofNat, Imo1993P6.eFn, Imo1993P6.lasti
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, Fin, eq_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.tot_eFn line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, ZMod, OfNat.ofNat, Imo1993P6.tot, Imo1993P6.eFn
Proof uses: id, Eq.mpr, Finset.sum, Fin, Finset.univ, ite, Imo1993P6.lasti, Membership.mem, Finset, congrArg, Finset.sum_ite_eq', of_eq_true, Eq.trans, True, congrFun', ite_eq_left_of_eq_true, eq_self
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.L_eFn line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Fin, ZMod, OfNat.ofNat, Imo1993P6.L, Imo1993P6.eFn, HAdd.hAdd
Proof uses: funext, Eq.mpr, Imo1993P6.lasti, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos, id, congrArg, Imo1993P6.L_apply, Imo1993P6.eFn_lasti, ite, HSub.hSub, Membership.mem, Finset, LT.lt, Fin.isLt, Eq.mp and 15 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.roundInv line 530 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, LE.le, Eq, Prod.fst, Nat.iterate, Prod, Imo1993P6.zstep, Prod.mk, ite, LT.lt, Imo1993P6.L
Proof uses: Nat.recAux, funext, id, Eq.mpr, congrArg, ite_eq_right, Nat.not_lt_zero, Eq.refl, HAdd.hAdd, Nat.succ, Function.iterate_succ_apply', Prod.snd, Fin.NatCast.instNatCast, Imo1993P6.pos_lemma, Function.update, HSub.hSub, congrFun', congr, zero_add, Fin.instAddMonoidWithOne and 47 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.round One full round of the process applies L and returns to position 0 line 591 source
Source documentation
One full round of the process applies L and returns to position 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Prod, Nat.iterate, Imo1993P6.zstep, Prod.mk, Imo1993P6.L
Proof uses: Prod.ext, Eq.mpr, Prod.fst, ite, LT.lt, id, congrArg, Imo1993P6.roundInv, le_refl, funext, ite_eq_left, Fin.isLt, Eq.refl, Prod.snd, HAdd.hAdd, Fin.NatCast.instNatCast, Imo1993P6.pos_lemma, Fin.natCast_self, Fin.instAddMonoidWithOne, add_zero
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma round {n : ℕ} [NeZero n] (x : Fin n → ZMod 2) :
    zstep^[n] (x, 0) = (L x, (0 : Fin n)) := by
…
```
Mentions: Imo1993P6.zstep, Imo1993P6.L
lemma Imo1993P6.aux line 600 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Prod, Fin, ZMod, OfNat.ofNat, Nat.iterate, Imo1993P6.zstep, Imo1993P6.zinit, Prod.mk, Imo1993P6.L
Proof uses: Nat.recAux, Eq.refl, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.succ, Function.iterate_succ_apply', Imo1993P6.round
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo1993P6.cat Concatenation of two lamp vectors line 610 source
Source documentation
Concatenation of two lamp vectors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, OfNat.ofNat, HAdd.hAdd
Proof uses: dite, LT.lt, Fin.mk, Not, HSub.hSub
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def cat {n : ℕ} (y z : Fin n → ZMod 2) : Fin (n + n) → ZMod 2 :=
…
```
lemma Imo1993P6.tot_cat line 613 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, Imo1993P6.tot, HAdd.hAdd, Imo1993P6.cat
Proof uses: NeZero.mk, Ne, NeZero.ne, Eq.mpr, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos, id, congrArg, Imo1993P6.tot_eq, Finset.sum_range_add, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.mp, LT.lt and 12 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.catL line 658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, Eq, HAdd.hAdd, Imo1993P6.L, Imo1993P6.cat, Imo1993P6.lasti, Imo1993P6.tot
Proof uses: NeZero.mk, Ne, NeZero.ne, funext, Eq.mpr, Finset.sum, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos, id, congrArg, Imo1993P6.L_apply, dite, LT.lt, Not, HSub.hSub, dite_eq_right, Imo1993P6.lasti_val and 26 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
def Imo1993P6.A line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: Eq, Fin, ZMod, OfNat.ofNat, Nat.iterate, Imo1993P6.L, HSub.hSub, Imo1993P6.eFn
15 instances, coercions and auxiliary constants left out.
def Imo1993P6.B line 763 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: LE.le, HSub.hSub, OfNat.ofNat, Eq, ZMod, Imo1993P6.tot, Nat.iterate, Fin, Imo1993P6.L
21 instances, coercions and auxiliary constants left out.
def Imo1993P6.C line 766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: LE.le, HSub.hSub, OfNat.ofNat, Eq, ZMod, Nat.iterate, Fin, Imo1993P6.L, Imo1993P6.lasti
16 instances, coercions and auxiliary constants left out.
def Imo1993P6.D Lamp n-2 is off at every positive round m ≤ n-1 line 770 source
Source documentation
Lamp n-2 is off at every positive round m ≤ n-1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: LE.le, OfNat.ofNat, HSub.hSub, Eq, ZMod, Nat.iterate, Fin, Imo1993P6.L, Fin.mk
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def D (n : ℕ) [NeZero n] : Prop :=
…
```
lemma Imo1993P6.base_case line 773 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Imo1993P6.A, OfNat.ofNat, Nat, Imo1993P6.B, Imo1993P6.C, Imo1993P6.D
Proof uses: And.intro, id, of_decide_eq_true, Eq, Fin, ZMod, Nat.iterate, Imo1993P6.L, HSub.hSub, Imo1993P6.eFn, Bool, Decidable.decide, Bool.true, Eq.refl, LE.le, Imo1993P6.tot, Eq.symm, dite, Imo1993P6.lasti, le_antisymm and 10 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P6.stepLemma line 791 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, Imo1993P6.A, Imo1993P6.B, Imo1993P6.C, Imo1993P6.D, And, HAdd.hAdd
Proof uses: NeZero.mk, Ne, NeZero.ne, HSub.hSub, Eq, Fin, ZMod, Nat.iterate, Imo1993P6.L, Imo1993P6.cat, Nat.recAux, funext, id, dite, LT.lt, Fin.mk, Not, Eq.mpr, congrArg, dite_eq_left and 38 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 237 steps (first 200 of 237)
Open to load the checked before-and-after goal states.
theorem Imo1993P6.core line 983 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NeZero, Eq, HPow.hPow, And, Imo1993P6.A, Imo1993P6.B, Imo1993P6.C, Imo1993P6.D
Proof uses: Nat.recAux, absurd, of_decide_eq_true, Not, id, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, Nat.casesAuxOn, Imo1993P6.base_case, Eq.symm, Eq.mp, congrArg, pow_one, NeZero.mk, pow_ne_zero, Ne, rfl and 9 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
theorem Imo1993P6.last_lamp_only_of_two_pow line 1002 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Eq, HPow.hPow, Fin, Bool, Imo1993P6.lampsAfter, HMul.hMul, HSub.hSub, Decidable.decide
Proof uses: Imo1993P6.A, And.left, And, Imo1993P6.B, Imo1993P6.C, Imo1993P6.D, Imo1993P6.core, rfl, id, Prod.fst, Nat.iterate, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial, Imo1993P6.z2b, ZMod, Prod, Imo1993P6.zstep, Imo1993P6.zinit, congrFun and 36 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def Imo1993P6.cStateVec State of the n'+1-lamp process of "shifted" form: lamp 0 off, lamp 1 on, and lamps 2..n' given by the vector x on Fin n' line 1029 source
Source documentation
State of the n'+1-lamp process of "shifted" form: lamp 0 off, lamp 1 on, and lamps 2..n' given by the vector x on Fin n'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, OfNat.ofNat, HAdd.hAdd
Proof uses: ite, Eq, dite, LE.le, Fin.mk, HSub.hSub, Not
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def cStateVec {n' : ℕ} [NeZero n'] (x : Fin n' → ZMod 2) : Fin (n' + 1) → ZMod 2 :=
…
```
lemma Imo1993P6.LcState Documented declaration: LcState line 1036 source
Source documentation
One round of the n'+1-process maps a shifted state to the shifted state of L x, provided x's last-but-one lamp is off (so lamp 0 stays off) and x's last lamp is on (so lamp 2's wrap-around toggle matches lamp 0 of the n'-process).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, HAdd.hAdd, OfNat.ofNat, LE.le, Fin, ZMod, Eq, Fin.mk, HSub.hSub, Imo1993P6.lasti, Imo1993P6.L, Imo1993P6.cStateVec
Proof uses: funext, Eq.mpr, Finset.sum, Finset.range, HMod.hMod, Nat.mod_lt, NeZero.pos, id, congrArg, Imo1993P6.L_apply, ite, dite, Not, ite_eq_right, dite_eq_left, LT.lt, Fin.ext, Eq.refl, zero_add, Nat.zero_mod and 23 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 92 steps
Open to load the checked before-and-after goal states.
```
lemma LcState {n' : ℕ} [NeZero n'] [NeZero (n' + 1)] (h2 : 2 ≤ n') (x : Fin n' → ZMod 2)
    (hα : x ⟨n' - 2, by have := NeZero.pos n'; lia⟩ = 0) (hβ : x (lasti n') = 1) :
…
```
Mentions: Imo1993P6.lasti
lemma Imo1993P6.L_one One round from the all-on state gives the alternating vector line 1116 source
Source documentation
One round from the all-on state gives the alternating vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, Fin, ZMod, OfNat.ofNat, Imo1993P6.L
Proof uses: funext, Eq.mpr, HAdd.hAdd, Finset.sum, Finset.range, id, congrArg, Imo1993P6.L_apply, Membership.mem, Finset, Fin.mk, HMod.hMod, Nat.mod_lt, NeZero.pos, rfl, Finset.sum_congr, HSMul.hSMul, Finset.card, Finset.sum_const, Finset.card_range and 9 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma L_one {n : ℕ} [NeZero n] :
    L ((fun _ => (1 : ZMod 2)) : Fin n → ZMod 2) = fun p => (p.val : ZMod 2) := by
…
```
Mentions: Imo1993P6.L
lemma Imo1993P6.invC The round-level invariant of part (c): after m rounds (1 ≤ m ≤ 2^k - 1), the (2^k+1)-process is in shifted form line 1129 source
Source documentation
The round-level invariant of part (c): after m rounds (1 ≤ m ≤ 2^k - 1), the (2^k+1)-process is in shifted form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HSub.hSub, HPow.hPow, Eq, Fin, HAdd.hAdd, ZMod, Nat.iterate, Imo1993P6.L, Imo1993P6.cStateVec
Proof uses: NeZero, NeZero.mk, pow_ne_zero, of_decide_eq_true, Ne, id, Bool, Decidable.decide, Bool.true, Eq.refl, ne_of_gt, add_pos', pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.ble, And, Imo1993P6.A, Imo1993P6.B, Imo1993P6.C and 33 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma invC (k : ℕ) (hk : 1 ≤ k) :
    ∀ m, 1 ≤ m → m ≤ 2 ^ k - 1 →
      L^[m] ((fun _ => (1 : ZMod 2)) : Fin (2 ^ k + 1) → ZMod 2)
        = cStateVec (L^[m] ((fun _ => (1 : ZMod 2)) : Fin (2 ^ k) → ZMod 2)) := by
…
```
Mentions: Imo1993P6.L, Imo1993P6.cStateVec
lemma Imo1993P6.cState_eFn The shifted state of eFn (2^k) is exactly "only lamp 1 on" line 1178 source
Source documentation
The shifted state of eFn (2^k) is exactly "only lamp 1 on".

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Fin, HAdd.hAdd, HPow.hPow, ZMod, Imo1993P6.cStateVec, Imo1993P6.eFn, ite
Proof uses: NeZero, NeZero.mk, pow_ne_zero, of_decide_eq_true, Ne, id, Bool, Decidable.decide, Bool.true, Eq.refl, ne_of_gt, add_pos', pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.ble, Nat.le_pow, funext, dite, Fin.mk and 13 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma cState_eFn (k : ℕ) (hk : 1 ≤ k) :
    cStateVec (eFn (2 ^ k)) = fun i => if i.val = 1 then (1 : ZMod 2) else 0 := by
…
```
Mentions: Imo1993P6.cStateVec, Imo1993P6.eFn
theorem Imo1993P6.lamp1_only_of_two_pow_add_one line 1200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Fin, Bool, Imo1993P6.lampsAfter, HMul.hMul, HSub.hSub, Decidable.decide
Proof uses: LE.le, And, Imo1993P6.A, Imo1993P6.B, Imo1993P6.C, Imo1993P6.D, Imo1993P6.core, rfl, Nat.le_pow, ZMod, Nat.iterate, Imo1993P6.L, Imo1993P6.cStateVec, Imo1993P6.invC, le_refl, id, Prod.fst, Imo1993P6.State, Imo1993P6.step, Imo1993P6.initial and 36 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
problem Imo1993P6.imo1993_p6_a line 1226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, Exists, And, Fin, Eq, Bool, Imo1993P6.lampsAfter, Bool.true
Proof uses: Imo1993P6.State, Nat.iterate, Imo1993P6.step, Imo1993P6.initial, Imo1993P6.step_periodic, Exists.intro, And.intro, id, Eq.mpr, Prod.fst, congrArg, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
problem Imo1993P6.imo1993_p6_b line 1233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, HPow.hPow, OfNat.ofNat, LT.lt, Fin, Bool, Imo1993P6.lampsAfter, HSub.hSub, Bool.true
Proof uses: LE.le, Trans.trans, Eq.symm, pow_one, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, Imo1993P6.all_on_of_last_only, Imo1993P6.last_lamp_only_of_two_pow
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
problem Imo1993P6.imo1993_p6_c line 1242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, LT.lt, Fin, Bool, Imo1993P6.lampsAfter, HSub.hSub, Bool.true
Proof uses: LE.le, Trans.trans, Eq.symm, pow_one, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, Imo1993P6.all_on_of_lamp1_only, Imo1993P6.lamp1_only_of_two_pow_add_one
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.