Theorem: Lean4Axiomatic.Natural.le_antisymm (Lean4Axiomatic/Natural/Order.lean)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n ≤ m → m ≤ n → n ≃ m
Tactic:
intro (_ : n ≤ m) (_ : m ≤ n)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
⊢ n ≃ m
Tactic:
have ⟨d₁, (_ : n + d₁ ≃ m)⟩ := le_defn.mp ‹n ≤ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝ : n + d₁ ≃ m
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝ : n + d₁ ≃ m
⊢ n ≃ m
Tactic:
have ⟨d₂, (_ : m + d₂ ≃ n)⟩ := le_defn.mp ‹m ≤ n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
⊢ n ≃ m
Tactic:
have : n + (d₁ + d₂) ≃ n + 0 := calc
  n + (d₁ + d₂) ≃ _ := Rel.symm AA.assoc
  (n + d₁) + d₂ ≃ _ := AA.substL ‹n + d₁ ≃ m›
  m + d₂        ≃ _ := ‹m + d₂ ≃ n›
  n             ≃ _ := Rel.symm add_zero
  n + 0         ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this : n + (d₁ + d₂) ≃ n + 0
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this : n + (d₁ + d₂) ≃ n + 0
⊢ n ≃ m
Tactic:
have : d₁ + d₂ ≃ 0 := AA.cancelL ‹n + (d₁ + d₂) ≃ n + 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
⊢ n ≃ m
Tactic:
have ⟨(_ : d₁ ≃ 0), _⟩ := zero_sum_split ‹d₁ + d₂ ≃ 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
left✝ : d₁ ≃ 0
right✝ : d₂ ≃ 0
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
left✝ : d₁ ≃ 0
right✝ : d₂ ≃ 0
⊢ n ≃ m
Tactic:
calc
  n      ≃ _ := Rel.symm add_zero
  n + 0  ≃ _ := AA.substR (Rel.symm ‹d₁ ≃ 0›)
  n + d₁ ≃ _ := ‹n + d₁ ≃ m›
  m      ≃ _ := Rel.refl
State after:
no goals