Theorem: Lean4Axiomatic.Rational.div_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 : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≄ 0 → p / q ≄ 0
Tactic:
intro (_ : p ≄ 0) (_ : p/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 : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
⊢ False

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
x✝ : p / q ≃ 0
⊢ False
Tactic:
have : p ≃ 0 := div_eqv_0.mp ‹p/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 : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
this : p ≃ 0
⊢ False

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
x✝ : p / q ≃ 0
this : p ≃ 0
⊢ False
Tactic:
exact absurd ‹p ≃ 0› ‹p ≄ 0›
State after:
no goals