Theorem: Lean4Axiomatic.Rational.sqrt1_nonzero (Lean4Axiomatic/Rational/Negation.lean)

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ Sqrt1 p → p ≄ 0
Tactic:
intro (_ : Sqrt1 p) (_ : p ≃ 0)
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
⊢ False
Tactic:
have : (1 : ℚ) ≃ 0 := calc
  (1 : ℚ) ≃ _ := eqv_symm ‹Sqrt1 p›.elim
  p * p   ≃ _ := mul_substL ‹p ≃ 0›
  0 * p   ≃ _ := mul_absorbL
  0       ≃ _ := eqv_refl
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this : 1 ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this : 1 ≃ 0
⊢ False
Tactic:
have : (1 : ℚ) ≄ 0 := nonzero_one
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℚ) ≃ 0› ‹(1 : ℚ) ≄ 0›
State after:
no goals