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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → p₁ * q ≃ p₂ * q
Tactic:
intro (p₁n//p₁d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Tactic:
revert p₂
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Tactic:
intro (p₂n//p₂d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ ∀ {q : Fraction ℤ}, p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ ∀ {q : Fraction ℤ}, p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Tactic:
intro (qn//qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Tactic:
intro (_ : p₁n//p₁d ≃ p₂n//p₂d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Tactic:
show (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)
Tactic:
show (p₁n * qn) * (p₂d * qd) ≃ (p₂n * qn) * (p₁d * qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Tactic:
have : p₁n * p₂d ≃ p₂n * p₁d := ‹p₁n//p₁d ≃ p₂n//p₂d›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Tactic:
calc
  (p₁n * qn) * (p₂d * qd) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (p₁n * p₂d) * (qn * qd) ≃ _ := AA.substL ‹p₁n * p₂d ≃ p₂n * p₁d›
  (p₂n * p₁d) * (qn * qd) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (p₂n * qn) * (p₁d * qd) ≃ _ := Rel.refl
State after:
no goals