Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL (Lean4Axiomatic/Integer/Impl/Difference/Addition.lean)

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → n——m + b ≃ a₂ + b
Tactic:
intro (k——j)
State after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m + b ≃ k——j + b

State before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m + b ≃ k——j + b
Tactic:
revert b
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ ∀ {b : Difference ℕ}, n——m ≃ k——j → n——m + b ≃ k——j + b

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ ∀ {b : Difference ℕ}, n——m ≃ k——j → n——m + b ≃ k——j + b
Tactic:
intro (p——q)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
⊢ n——m ≃ k——j → n——m + p——q ≃ k——j + p——q

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
⊢ n——m ≃ k——j → n——m + p——q ≃ k——j + p——q
Tactic:
intro (_ : n——m ≃ k——j)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m + p——q ≃ k——j + p——q

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m + p——q ≃ k——j + p——q
Tactic:
have : n + j ≃ k + m := ‹n——m ≃ k——j›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n——m + p——q ≃ k——j + p——q

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n——m + p——q ≃ k——j + p——q
Tactic:
show (n + p)——(m + q) ≃ (k + p)——(j + q)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ (n + p)——(m + q) ≃ (k + p)——(j + q)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ (n + p)——(m + q) ≃ (k + p)——(j + q)
Tactic:
show (n + p) + (j + q) ≃ (k + p) + (m + q)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n + p + (j + q) ≃ k + p + (m + q)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n + p + (j + q) ≃ k + p + (m + q)
Tactic:
calc
  (n + p) + (j + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (n + j) + (p + q) ≃ _ := AA.substL ‹n + j ≃ k + m›
  (k + m) + (p + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (k + p) + (m + q) ≃ _ := Rel.refl
State after:
no goals