Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans (Lean4Axiomatic/Integer/Impl/Difference/Core.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
a b c : Difference ℕ
⊢ a ≃ b → b ≃ c → a ≃ c
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ c → a ≃ c

State before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ c → a ≃ c
Tactic:
intro (a₁——a₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c

State before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Tactic:
revert b
State after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c

State before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Tactic:
intro (b₁——b₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c

State before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Tactic:
revert c
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ ∀ {c : Difference ℕ}, a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ ∀ {c : Difference ℕ}, a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Tactic:
intro (c₁——c₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c₁——c₂ → a₁——a₂ ≃ c₁——c₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c₁——c₂ → a₁——a₂ ≃ c₁——c₂
Tactic:
intro (_ : a₁ + b₂ ≃ b₁ + a₂) (_ : b₁ + c₂ ≃ c₁ + b₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁——a₂ ≃ c₁——c₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁——a₂ ≃ c₁——c₂
Tactic:
show a₁ + c₂ ≃ c₁ + a₂
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁ + c₂ ≃ c₁ + a₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁ + c₂ ≃ c₁ + a₂
Tactic:
have : (a₁ + c₂) + (b₂ + b₁) ≃ (c₁ + a₂) + (b₂ + b₁) := calc
  (a₁ + c₂) + (b₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (a₁ + b₂) + (c₂ + b₁) ≃ _ := AA.substL ‹a₁ + b₂ ≃ b₁ + a₂›
  (b₁ + a₂) + (c₂ + b₁) ≃ _ := AA.substL AA.comm
  (a₂ + b₁) + (c₂ + b₁) ≃ _ := AA.substR AA.comm
  (a₂ + b₁) + (b₁ + c₂) ≃ _ := AA.substR ‹b₁ + c₂ ≃ c₁ + b₂›
  (a₂ + b₁) + (c₁ + b₂) ≃ _ := AA.comm
  (c₁ + b₂) + (a₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (c₁ + a₂) + (b₂ + b₁) ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
this : a₁ + c₂ + (b₂ + b₁) ≃ c₁ + a₂ + (b₂ + b₁)
⊢ a₁ + c₂ ≃ c₁ + a₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
this : a₁ + c₂ + (b₂ + b₁) ≃ c₁ + a₂ + (b₂ + b₁)
⊢ a₁ + c₂ ≃ c₁ + a₂
Tactic:
exact AA.cancelR ‹(a₁ + c₂) + (b₂ + b₁) ≃ (c₁ + a₂) + (b₂ + b₁)›
State after:
no goals