Theorem: Lean4Axiomatic.Rational.add_div_integers (Lean4Axiomatic/Rational/Sign.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
Tactic:
let aQ := (a : ℚ)
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
Tactic:
let bQ := (b : ℚ)
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
Tactic:
let cQ := (c : ℚ)
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
cQ : ℚ := from_integer c
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
cQ : ℚ := from_integer c
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
Tactic:
let dQ := (d : ℚ)
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
cQ : ℚ := from_integer c
dQ : ℚ := from_integer d
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
cQ : ℚ := from_integer c
dQ : ℚ := from_integer d
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
Tactic:
calc
  aQ/bQ + cQ/dQ
    ≃ _ := add_substL div_mul_recip
  aQ * bQ⁻¹ + cQ/dQ
    ≃ _ := add_substR div_mul_recip
  aQ * bQ⁻¹ + cQ * dQ⁻¹
    ≃ _ := add_substL (eqv_symm mul_identR)
  aQ * bQ⁻¹ * 1 + cQ * dQ⁻¹
    ≃ _ := add_substL (mul_substR (eqv_symm mul_inverseR))
  aQ * bQ⁻¹ * (dQ * dQ⁻¹) + cQ * dQ⁻¹
    ≃ _ := add_substL AA.expr_xxfxxff_lr_swap_rl
  aQ * dQ * (bQ⁻¹ * dQ⁻¹) + cQ * dQ⁻¹
    ≃ _ := add_substL (mul_substR (eqv_symm recip_compat_mul))
  aQ * dQ * (bQ * dQ)⁻¹ + cQ * dQ⁻¹
    ≃ _ := add_substR (eqv_symm mul_identR)
  aQ * dQ * (bQ * dQ)⁻¹ + cQ * dQ⁻¹ * 1
    ≃ _ := add_substR (mul_substR (eqv_symm mul_inverseL))
  aQ * dQ * (bQ * dQ)⁻¹ + cQ * dQ⁻¹ * (bQ⁻¹ * bQ)
    ≃ _ := add_substR AA.expr_xxfxxff_lr_swap_rr
  aQ * dQ * (bQ * dQ)⁻¹ + cQ * bQ * (bQ⁻¹ * dQ⁻¹)
    ≃ _ := add_substR (mul_substL mul_comm)
  aQ * dQ * (bQ * dQ)⁻¹ + bQ * cQ * (bQ⁻¹ * dQ⁻¹)
    ≃ _ := add_substR (mul_substR (eqv_symm recip_compat_mul))
  aQ * dQ * (bQ * dQ)⁻¹ + bQ * cQ * (bQ * dQ)⁻¹
    ≃ _ := eqv_symm mul_distribR
  (aQ * dQ + bQ * cQ) * (bQ * dQ)⁻¹
    ≃ _ := mul_substL (add_substL (eqv_symm mul_compat_from_integer))
  ((a * d : ℤ) + bQ * cQ) * (bQ * dQ)⁻¹
    ≃ _ := mul_substL (add_substR (eqv_symm mul_compat_from_integer))
  ((a * d : ℤ) + (b * c : ℤ)) * (bQ * dQ)⁻¹
    ≃ _ := mul_substL (eqv_symm add_compat_from_integer)
  (a * d + b * c : ℤ) * (bQ * dQ)⁻¹
    ≃ _ := mul_substR (recip_subst (eqv_symm mul_compat_from_integer))
  (a * d + b * c : ℤ) * ((b * d : ℤ) : ℚ)⁻¹
    ≃ _ := eqv_symm div_mul_recip
  ((a * d + b * c : ℤ) : ℚ)/((b * d : ℤ) : ℚ)
    ≃ _ := eqv_refl
State after:
no goals