-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem scale_opowAux (e a0 a : ONote) [NF e] [NF a0] [NF a] :
    ∀ k m, repr (opowAux e a0 a k m) = ω ^ repr e * repr (opowAux 0 a0 a k m)
  | 0, m => by cases m <;> simp [opowAux]
  | k + 1, m => by
    by_cases h : m = 0
    · simp [h, opowAux, mul_add, opow_add, mul_assoc, scale_opowAux _ _ _ k]
    · -- Porting note: rewrote proof
      rw [opowAux]; swap
      · assumption
      rw [opowAux]; swap
      · assumption
      rw [repr_add, repr_scale, scale_opowAux _ _ _ k]
      simp only [repr_add, repr_scale, opow_add, mul_assoc, zero_add, mul_add]

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
rw [opowAux]

Result:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

Tactic:
swap

Result:
case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ω ^ (e + a0.mulNat k).repr * a.repr + ω ^ e.repr * (opowAux 0 a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

Tactic:
simp only [repr_add, repr_scale, opow_add, mul_assoc, zero_add, mul_add]

Result:
no goals

Proof state:
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
by_cases h : m = 0

Result:
case pos
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Proof state:
case pos
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
simp [h, opowAux, mul_add, opow_add, mul_assoc, scale_opowAux _ _ _ k]

Result:
no goals

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

Tactic:
rw [repr_add, repr_scale, scale_opowAux _ _ _ k]

Result:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ω ^ (e + a0.mulNat k).repr * a.repr + ω ^ e.repr * (opowAux 0 a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

Proof state:
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m : ℕ
⊢ (e.opowAux a0 a 0 m).repr = ω ^ e.repr * (opowAux 0 a0 a 0 m).repr

Tactic:
cases m <;> simp [opowAux]

Result:
no goals

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

Tactic:
swap

Result:
case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr =
    ω ^ e.repr * ((0 + a0.mulNat k).scale a + opowAux 0 a0 a k m).repr

Proof state:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
rw [opowAux]

Result:
case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ ((e + a0.mulNat k).scale a + e.opowAux a0 a k m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

Proof state:
case neg.x_2
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ m = 0 → False

Tactic:
assumption

Result:
no goals