Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_compat_from_integer (Lean4Axiomatic/Rational/Impl/Fraction/Addition.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ from_integer (a + b) ≃ from_integer a + from_integer b
Tactic:
show (a + b)//1 ≃ a//1 + b//1
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a + b)//1 ≃ a//1 + b//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a + b)//1 ≃ a//1 + b//1
Tactic:
have : a//1 + b//1 ≃ (a + b)//1 := calc
  a//1 + b//1              ≃ _ := eqv_refl
  (a * 1 + 1 * b)//(1 * 1) ≃ _ := substN (AA.substL AA.identR)
  (a + 1 * b)//(1 * 1)     ≃ _ := substN (AA.substR AA.identL)
  (a + b)//(1 * 1)         ≃ _ := substD AA.identL
  (a + b)//1               ≃ _ := eqv_refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
this : a//1 + b//1 ≃ (a + b)//1
⊢ (a + b)//1 ≃ a//1 + b//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
this : a//1 + b//1 ≃ (a + b)//1
⊢ (a + b)//1 ≃ a//1 + b//1
Tactic:
exact eqv_symm this
State after:
no goals