Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq (Arithmetization/ISigmaZero/Exponential/PPow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
⊢ i = j
Tactic:
by_contra ne
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
⊢ False
Tactic:
wlog hij : i < j
State after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
⊢ False

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
⊢ False
Tactic:
have : y^2 < y^2 := calc
  y^2 < i^2 := sq_lt_sq.mpr hi.1
  _   ≤ j   := sq_le_of_lt ppi ppj hij
  _   ≤ y^2 := hj.2
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
this : y ^ 2 < y ^ 2
⊢ False

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
this : y ^ 2 < y ^ 2
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False
Tactic:
exact this py ppj ppi hj hi (Ne.symm ne) (Ne.lt_of_le' ne (by simpa using hij))
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 ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ j ≤ i
Tactic:
simpa using hij
State after:
no goals