Theorem: Lean4Axiomatic.Rational.mul_preserves_nonzero (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 ℚ
p q : ℚ
⊢ p ≄ 0 → q ≄ 0 → p * q ≄ 0
Tactic:
intro (_ : p ≄ 0) (_ : q ≄ 0)
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

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›
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

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
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

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
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

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
State after:
no goals