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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * (q + r) ≃ p * q + p * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * 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 + pn//pd * rn//rd
Tactic:
have pos_mul_denom_prq : AP (Positive (pd * (rd * qd))) := inferInstance
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)
pos_mul_denom_prq : AP (Positive (pd * (rd * qd)))
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * 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)
pos_mul_denom_prq : AP (Positive (pd * (rd * qd)))
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
Tactic:
calc
  pn//pd * (qn//qd + rn//rd)
    ≃ _ := eqv_refl
  pn//pd * (qn * rd + qd * rn)//(qd * rd)
    ≃ _ := eqv_refl
  (pn * (qn * rd + qd * rn))//(pd * (qd * rd))
    ≃ _ := substN AA.distribL
  (pn * (qn * rd) + pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := eqv_symm add_eqv_denominators
  (pn * (qn * rd))//(pd * (qd * rd)) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL (substN (Rel.symm AA.assoc))
  ((pn * qn) * rd)//(pd * (qd * rd)) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL (substD (Rel.symm AA.assoc))
  ((pn * qn) * rd)//((pd * qd) * rd) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL cancelR
  (pn * qn)//(pd * qd) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substR (substN (AA.substR AA.comm))
  (pn * qn)//(pd * qd) + (pn * (rn * qd))//(pd * (qd * rd))
    ≃ _ := add_substR (substD (pb₂ := pos_mul_denom_prq) (AA.substR AA.comm))
  (pn * qn)//(pd * qd) + (pn * (rn * qd))//(pd * (rd * qd))
    ≃ _ := add_substR (substN (Rel.symm AA.assoc))
  (pn * qn)//(pd * qd) + ((pn * rn) * qd)//(pd * (rd * qd))
    ≃ _ := add_substR (substD (Rel.symm AA.assoc))
  (pn * qn)//(pd * qd) + ((pn * rn) * qd)//((pd * rd) * qd)
    ≃ _ := add_substR cancelR
  (pn * qn)//(pd * qd) + (pn * rn)//(pd * rd)
    ≃ _ := eqv_refl
  pn//pd * qn//qd + (pn * rn)//(pd * rd)
    ≃ _ := eqv_refl
  pn//pd * qn//qd + pn//pd * rn//rd
    ≃ _ := eqv_refl
State after:
no goals