Theorem: Lean4Axiomatic.Integer.one_neqv_zero (Lean4Axiomatic/Integer/Core.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
⊢ 1 ≄ 0
Tactic:
intro (_ : (1 : ℤ) ≃ 0)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
⊢ False
Tactic:
have : coe (1 : ℕ) ≃ coe (0 : ℕ) := ‹(1 : ℤ) ≃ 0›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this : coe 1 ≃ coe 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this : coe 1 ≃ coe 0
⊢ False
Tactic:
have : (1 : ℕ) ≃ 0 := AA.inject ‹coe (1 : ℕ) ≃ coe (0 : ℕ)›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False
Tactic:
have : Natural.step (0 : ℕ) ≃ 0 :=
  Rel.trans (Rel.symm Natural.literal_step) ‹(1 : ℕ) ≃ 0›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False
Tactic:
exact absurd ‹Natural.step (0 : ℕ) ≃ 0› Natural.step_neqv_zero
State after:
no goals