internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this✝¹ : sgn p * sgn q ≃ 0
this✝ : sgn p ≃ 0 ∨ sgn q ≃ 0
this : p ≃ 0 ∨ q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p ≃ 0 ∨ q ≃ 0 → p * q ≃ 0
Tactic:
intro (_ : p ≃ 0 ∨ q ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p ≃ 0 ∨ q ≃ 0
⊢ p * q ≃ 0
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p ≃ 0 ∨ q ≃ 0
⊢ p * q ≃ 0
Tactic:
match ‹p ≃ 0 ∨ q ≃ 0› with
| Or.inl (_ : p ≃ 0) => calc
  p * q ≃ _ := mul_substL ‹p ≃ 0›
  0 * q ≃ _ := mul_absorbL
  0     ≃ _ := eqv_refl
| Or.inr (_ : q ≃ 0) => calc
  p * q ≃ _ := mul_substR ‹q ≃ 0›
  p * 0 ≃ _ := mul_absorbR
  0     ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p ≃ 0 ∨ q ≃ 0
h✝ : p ≃ 0
⊢ p * q ≃ 0
Tactic:
calc
p * q ≃ _ := mul_substL ‹p ≃ 0›
0 * q ≃ _ := mul_absorbL
0     ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p ≃ 0 ∨ q ≃ 0
h✝ : q ≃ 0
⊢ p * q ≃ 0
Tactic:
calc
p * q ≃ _ := mul_substR ‹q ≃ 0›
p * 0 ≃ _ := mul_absorbR
0     ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p ≄ 0 → q ≄ 0 → p * q ≄ 0
Tactic:
intro (_ : p ≄ 0) (_ : q ≄ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
⊢ p * q ≄ 0
Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
⊢ p * q ≄ 0
Tactic:
have : p ≄ 0 ∧ q ≄ 0 := And.intro ‹p ≄ 0› ‹q ≄ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this : p ≄ 0 ∧ q ≄ 0
⊢ p * q ≄ 0
Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this : p ≄ 0 ∧ q ≄ 0
⊢ p * q ≄ 0
Tactic:
have : ¬(p ≃ 0 ∨ q ≃ 0) := Logic.not_or_iff_and_not.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this✝ : p ≄ 0 ∧ q ≄ 0
this : ¬(p ≃ 0 ∨ q ≃ 0)
⊢ p * q ≄ 0
Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this✝ : p ≄ 0 ∧ q ≄ 0
this : ¬(p ≃ 0 ∨ q ≃ 0)
⊢ p * q ≄ 0
Tactic:
have : p * q ≄ 0 := mt mul_split_zero.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this✝¹ : p ≄ 0 ∧ q ≄ 0
this✝ : ¬(p ≃ 0 ∨ q ≃ 0)
this : p * q ≄ 0
⊢ p * q ≄ 0
Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝¹ : p ≄ 0
x✝ : q ≄ 0
this✝¹ : p ≄ 0 ∧ q ≄ 0
this✝ : ¬(p ≃ 0 ∨ q ≃ 0)
this : p * q ≄ 0
⊢ p * q ≄ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.recip_compat_mul
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have inv_p : 1 ≃ p * p⁻¹ := eqv_symm mul_inverseR
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Theorem: Lean4Axiomatic.Rational.recip_compat_mul
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have inv_q : 1 ≃ q * q⁻¹ := eqv_symm mul_inverseR
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Theorem: Lean4Axiomatic.Rational.recip_compat_mul
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have swap_middle : (p * p⁻¹) * (q * q⁻¹) ≃ (p * q) * (p⁻¹ * q⁻¹) :=
  AA.expr_xxfxxff_lr_swap_rl
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
swap_middle : p * p⁻¹ * (q * q⁻¹) ≃ p * q * (p⁻¹ * q⁻¹)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Theorem: Lean4Axiomatic.Rational.recip_compat_mul
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
swap_middle : p * p⁻¹ * (q * q⁻¹) ≃ p * q * (p⁻¹ * q⁻¹)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
calc
  (p * q)⁻¹                           ≃ _ := eqv_symm mul_identR
  (p * q)⁻¹ * 1                       ≃ _ := mul_substR (eqv_symm mul_identR)
  (p * q)⁻¹ * (1 * 1)                 ≃ _ := mul_substR (mul_substL inv_p)
  (p * q)⁻¹ * ((p * p⁻¹) * 1)         ≃ _ := mul_substR (mul_substR inv_q)
  (p * q)⁻¹ * ((p * p⁻¹) * (q * q⁻¹)) ≃ _ := mul_substR swap_middle
  (p * q)⁻¹ * ((p * q) * (p⁻¹ * q⁻¹)) ≃ _ := eqv_symm mul_assoc
  ((p * q)⁻¹ * (p * q)) * (p⁻¹ * q⁻¹) ≃ _ := mul_substL mul_inverseL
  1 * (p⁻¹ * q⁻¹)                     ≃ _ := mul_identL
  p⁻¹ * q⁻¹                           ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.add_div_integers
Proof 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 : ℚ)
Proof 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)
Theorem: Lean4Axiomatic.Rational.add_div_integers
Proof 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 : ℚ)
Proof 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)
Theorem: Lean4Axiomatic.Rational.add_div_integers
Proof 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 : ℚ)
Proof 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)
Theorem: Lean4Axiomatic.Rational.add_div_integers
Proof 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 : ℚ)
Proof 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)
Theorem: Lean4Axiomatic.Rational.add_div_integers
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 0 ↔ p ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 0 → p ≃ 0

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ 0 → p / q ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 0 → p ≃ 0
Tactic:
case mp =>
  intro (_ : p/q ≃ 0)
  show p ≃ 0
  have : p * q⁻¹ ≃ 0 := eqv_trans (eqv_symm div_mul_recip) ‹p/q ≃ 0›
  have : p ≃ 0 ∨ q⁻¹ ≃ 0 := mul_split_zero.mp this
  match this with
  | Or.inl (_ : p ≃ 0) =>
    exact ‹p ≃ 0›
  | Or.inr (_ : q⁻¹ ≃ 0) =>
    have : q⁻¹ ≄ 0 := recip_preserves_nonzero
    exact absurd ‹q⁻¹ ≃ 0› ‹q⁻¹ ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ 0 → p / q ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ 0)
  show p/q ≃ 0
  calc
    _ ≃ p/q     := eqv_refl
    _ ≃ p * q⁻¹ := div_mul_recip
    _ ≃ 0 * q⁻¹ := mul_substL ‹p ≃ 0›
    _ ≃ 0       := mul_absorbL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 0 → p ≃ 0
Tactic:
intro (_ : p/q ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
⊢ p ≃ 0
Tactic:
have : p * q⁻¹ ≃ 0 := eqv_trans (eqv_symm div_mul_recip) ‹p/q ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this : p * q⁻¹ ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this : p * q⁻¹ ≃ 0
⊢ p ≃ 0
Tactic:
have : p ≃ 0 ∨ q⁻¹ ≃ 0 := mul_split_zero.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝ : p * q⁻¹ ≃ 0
this : p ≃ 0 ∨ q⁻¹ ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝ : p * q⁻¹ ≃ 0
this : p ≃ 0 ∨ q⁻¹ ≃ 0
⊢ p ≃ 0
Tactic:
match this with
| Or.inl (_ : p ≃ 0) =>
  exact ‹p ≃ 0›
| Or.inr (_ : q⁻¹ ≃ 0) =>
  have : q⁻¹ ≄ 0 := recip_preserves_nonzero
  exact absurd ‹q⁻¹ ≃ 0› ‹q⁻¹ ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝ : p * q⁻¹ ≃ 0
this : p ≃ 0 ∨ q⁻¹ ≃ 0
h✝ : p ≃ 0
⊢ p ≃ 0
Tactic:
exact ‹p ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝ : p * q⁻¹ ≃ 0
this : p ≃ 0 ∨ q⁻¹ ≃ 0
h✝ : q⁻¹ ≃ 0
⊢ p ≃ 0
Tactic:
have : q⁻¹ ≄ 0 := recip_preserves_nonzero
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝¹ : p * q⁻¹ ≃ 0
this✝ : p ≃ 0 ∨ q⁻¹ ≃ 0
h✝ : q⁻¹ ≃ 0
this : q⁻¹ ≄ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 0
this✝¹ : p * q⁻¹ ≃ 0
this✝ : p ≃ 0 ∨ q⁻¹ ≃ 0
h✝ : q⁻¹ ≃ 0
this : q⁻¹ ≄ 0
⊢ p ≃ 0
Tactic:
exact absurd ‹q⁻¹ ≃ 0› ‹q⁻¹ ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ 0 → p / q ≃ 0
Tactic:
intro (_ : p ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ 0
⊢ p / q ≃ 0
Theorem: Lean4Axiomatic.Rational.div_eqv_0
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ 0
⊢ p / q ≃ 0
Tactic:
calc
  _ ≃ p/q     := eqv_refl
  _ ≃ p * q⁻¹ := div_mul_recip
  _ ≃ 0 * q⁻¹ := mul_substL ‹p ≃ 0›
  _ ≃ 0       := mul_absorbL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_preserves_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≄ 0 → p / q ≄ 0
Tactic:
intro (_ : p ≄ 0) (_ : p/q ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
⊢ False