Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc (Lean4Axiomatic/Rational/Impl/Fraction/Multiplication.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ p * q * r ≃ p * (q * r)
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q * r ≃ p * (q * r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q * r ≃ p * (q * r)
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q * r ≃ pn//pd * (q * r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q * r ≃ pn//pd * (q * r)
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q * r ≃ pn//pd * (q * r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q * r ≃ pn//pd * (q * r)
Tactic:
intro (qn//qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Tactic:
revert r
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Tactic:
intro (rn//rd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * qn//qd * rn//rd ≃ pn//pd * (qn//qd * rn//rd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * qn//qd * rn//rd ≃ pn//pd * (qn//qd * rn//rd)
Tactic:
calc
  (pn//pd * qn//qd) * rn//rd         ≃ _ := eqv_refl
  (pn * qn)//(pd * qd) * rn//rd      ≃ _ := eqv_refl
  ((pn * qn) * rn)//((pd * qd) * rd) ≃ _ := substN AA.assoc
  (pn * (qn * rn))//((pd * qd) * rd) ≃ _ := substD AA.assoc
  (pn * (qn * rn))//(pd * (qd * rd)) ≃ _ := eqv_refl
  pn//pd * (qn * rn)//(qd * rd)      ≃ _ := eqv_refl
  pn//pd * (qn//qd * rn//rd)         ≃ _ := eqv_refl
State after:
no goals