Theorem: Nat.tri_add_inj (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ≤ n₁ → m₂ ≤ n₂ → n₁.tri + m₁ = n₂.tri + m₂ → n₁ = n₂
Tactic:
intro h₁ h₂ h
State after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
⊢ n₁ = n₂

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ = n₂
Tactic:
antisymmetry using LE.le
State after:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ ≤ n₂

case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₂ ≤ n₁

State before:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ ≤ n₂
Tactic:
exact hle
State after:
no goals

State before:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₂ ≤ n₁
Tactic:
exact hge
State after:
no goals

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ = n₂
Tactic:
absurd h
State after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Tactic:
apply Nat.ne_of_lt
State after:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ < n₂.tri + m₂

State before:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ < n₂.tri + m₂
Tactic:
transitivity (tri n₁ + n₁) using LE.le, LT.lt
State after:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ ≤ n₁.tri + n₁

case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri + m₂

State before:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ ≤ n₁.tri + n₁
Tactic:
apply Nat.add_le_add_left
State after:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ m₁ ≤ n₁

State before:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ m₁ ≤ n₁
Tactic:
exact h₁
State after:
no goals

State before:
case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri + m₂
Tactic:
transitivity (tri n₂) using LT.lt, LE.le
State after:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri

case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₂.tri ≤ n₂.tri + m₂

State before:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri
Tactic:
apply Nat.tri_add_self_lt_tri_of_lt
State after:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ < n₂

State before:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ < n₂
Tactic:
exact Nat.lt_of_not_ge hlt
State after:
no goals

State before:
case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₂.tri ≤ n₂.tri + m₂
Tactic:
exact Nat.le_add_right ..
State after:
no goals

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁ = n₂
Tactic:
absurd h
State after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Tactic:
symmetry using (.≠.)
State after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≠ n₁.tri + m₁

State before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≠ n₁.tri + m₁
Tactic:
apply Nat.ne_of_lt
State after:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ < n₁.tri + m₁

State before:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ < n₁.tri + m₁
Tactic:
transitivity (tri n₂ + n₂) using LE.le, LT.lt
State after:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≤ n₂.tri + n₂

case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri + m₁

State before:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≤ n₂.tri + n₂
Tactic:
apply Nat.add_le_add_left
State after:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ m₂ ≤ n₂

State before:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ m₂ ≤ n₂
Tactic:
exact h₂
State after:
no goals

State before:
case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri + m₁
Tactic:
transitivity (tri n₁) using LT.lt, LE.le
State after:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri

case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁.tri ≤ n₁.tri + m₁

State before:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri
Tactic:
apply Nat.tri_add_self_lt_tri_of_lt
State after:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂ < n₁

State before:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂ < n₁
Tactic:
exact Nat.gt_of_not_le hgt
State after:
no goals

State before:
case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁.tri ≤ n₁.tri + m₁
Tactic:
exact Nat.le_add_right ..
State after:
no goals