Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_compat_from_integer (Lean4Axiomatic/Rational/Impl/Fraction/Multiplication.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 * 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