Theorem: LO.FirstOrder.Arith.Model.ext_rem (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
⊢ ext i (z % j) = ext i z
Tactic:
have := div_add_mod z j
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this : j * (z / j) + z % j = z
⊢ ext i (z % j) = ext i z

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this : j * (z / j) + z % j = z
⊢ ext i (z % j) = ext i z
Tactic:
have : i^2 ∣ j := ppi.pow2.sq.dvd_of_le ppj.pow2 (PPow2.sq_le_of_lt ppi ppj hij)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i z

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i z
Tactic:
calc
  ext i (z % j) = ext i (j * (z / j) + (z % j)) := by symm; exact ext_add_of_dvd_sq_left ppi.pos (Dvd.dvd.mul_right this (z / j))
  _               = ext i z                          := by simp [div_add_mod]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i (j * (z / j) + z % j)
Tactic:
symm
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i (z % j)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i (z % j)
Tactic:
exact ext_add_of_dvd_sq_left ppi.pos (Dvd.dvd.mul_right this (z / j))
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i z
Tactic:
simp [div_add_mod]
State after:
no goals