Theorem: Lean4Axiomatic.Rational.recip_preserves_nonzero (Lean4Axiomatic/Rational/Reciprocation.lean)

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
⊢ p⁻¹ ≄ 0
Tactic:
intro (_ : p⁻¹ ≃ 0)
State after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
⊢ False
Tactic:
have : p ≃ 0 := calc
  _ ≃ p             := eqv_refl
  _ ≃ p * 1         := eqv_symm mul_identR
  _ ≃ p * (p * p⁻¹) := mul_substR (eqv_symm mul_inverseR)
  _ ≃ p * (p * 0)   := mul_substR (mul_substR ‹p⁻¹ ≃ 0›)
  _ ≃ p * 0         := mul_substR mul_absorbR
  _ ≃ 0             := mul_absorbR
State after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
this : p ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
this : p ≃ 0
⊢ False
Tactic:
exact absurd ‹p ≃ 0› ‹AP (p ≄ 0)›.ev
State after:
no goals