Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one (Lean4Axiomatic/Integer/Negation.lean)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ -1 ≄ 1
Tactic:
intro (_ : -1 ≃ (1 : ℤ))
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ False

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ False
Tactic:
have : step 0 ≃ 1 := Rel.symm Natural.literal_step
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this : step 0 ≃ 1
⊢ False

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this : step 0 ≃ 1
⊢ False
Tactic:
have : (step 1 : ℤ) ≃ (0 : ℤ) := calc
  (step 1 : ℤ)           ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
  (step (1 + 0) : ℤ)     ≃ _ := AA.subst₁ AA.scompatR
  ((1 + step 0 : ℕ) : ℤ) ≃ _ := AA.subst₁ (AA.substR ‹step 0 ≃ 1›)
  ((1 + 1 : ℕ) : ℤ)      ≃ _ := AA.compat₂
  (1 : ℤ) + (1 : ℤ)      ≃ _ := AA.substR (Rel.symm ‹-1 ≃ (1 : ℤ)›)
  1 + -1                 ≃ _ := AA.inverseR
  0                      ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝ : step 0 ≃ 1
this : coe (step 1) ≃ 0
⊢ False

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝ : step 0 ≃ 1
this : coe (step 1) ≃ 0
⊢ False
Tactic:
have : step 1 ≃ 0 := AA.inject ‹((step 1 : ℕ) : ℤ) ≃ ((0 : ℕ) : ℤ)›
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝¹ : step 0 ≃ 1
this✝ : coe (step 1) ≃ 0
this : step 1 ≃ 0
⊢ False

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝¹ : step 0 ≃ 1
this✝ : coe (step 1) ≃ 0
this : step 1 ≃ 0
⊢ False
Tactic:
have : step 1 ≄ 0 := Natural.step_neqv_zero
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝² : step 0 ≃ 1
this✝¹ : coe (step 1) ≃ 0
this✝ : step 1 ≃ 0
this : step 1 ≄ 0
⊢ False

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝² : step 0 ≃ 1
this✝¹ : coe (step 1) ≃ 0
this✝ : step 1 ≃ 0
this : step 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹step 1 ≃ 0› ‹step 1 ≄ 0›
State after:
no goals