Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right (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 ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ ext u (z₁ + z₂) = ext u z₁
Tactic:
simp [ext]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ (z₁ + z₂) / u % u = z₁ / u % u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Tactic:
have : ∃ z', z₂ = z' * u * u := by rcases h with ⟨u', rfl⟩; exact ⟨u', by simp [mul_comm _ u', mul_assoc]; simp [sq]⟩
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
this : ∃ z', z₂ = z' * u * u
⊢ (z₁ + z₂) / u % u = z₁ / u % u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
this : ∃ z', z₂ = z' * u * u
⊢ (z₁ + z₂) / u % u = z₁ / u % u
Tactic:
rcases this with ⟨z₂, rfl⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
z₂ : M
h : u ^ 2 ∣ z₂ * u * u
⊢ (z₁ + z₂ * u * u) / u % u = z₁ / u % u

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
z₂ : M
h : u ^ 2 ∣ z₂ * u * u
⊢ (z₁ + z₂ * u * u) / u % u = z₁ / u % u
Tactic:
simp [div_add_mul_self, pos]
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 ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ ∃ z', z₂ = z' * u * u
Tactic:
rcases h with ⟨u', rfl⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ ∃ z', u ^ 2 * u' = z' * u * u

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ ∃ z', u ^ 2 * u' = z' * u * u
Tactic:
exact ⟨u', by simp [mul_comm _ u', mul_assoc]; simp [sq]⟩
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 ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 * u' = u' * u * u
Tactic:
simp [mul_comm _ u', mul_assoc]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 = u * u ∨ u' = 0

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 = u * u ∨ u' = 0
Tactic:
simp [sq]
State after:
no goals