Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL (Lean4Axiomatic/Rational/Impl/Fraction/Addition.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✝ : Logic.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✝ : Logic.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✝ : Logic.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✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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 * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * 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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)

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