Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero (Lean4Axiomatic/Rational/Core.lean)

State before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
⊢ Integer.Nonzero a → from_integer a ≄ 0
Tactic:
intro (_ : Integer.Nonzero a) (_ : (a : ℚ) ≃ 0)
State after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
⊢ False
Tactic:
have : a ≄ 0 := Integer.nonzero_iff_neqv_zero.mp ‹Integer.Nonzero a›
State after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this : a ≄ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this : a ≄ 0
⊢ False
Tactic:
have : (a : ℚ) ≃ (0 : ℚ) := ‹(a : ℚ) ≃ 0›
State after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝ : a ≄ 0
this : from_integer a ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝ : a ≄ 0
this : from_integer a ≃ 0
⊢ False
Tactic:
have : a ≃ 0 := from_integer_inject this
State after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝¹ : a ≄ 0
this✝ : from_integer a ≃ 0
this : a ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝¹ : a ≄ 0
this✝ : from_integer a ≃ 0
this : a ≃ 0
⊢ False
Tactic:
exact absurd ‹a ≃ 0› ‹a ≄ 0›
State after:
no goals