Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a ↔ a ≄ 0
Tactic:
have (And.intro (_ : a ≃ 0 ∨ Nonzero a) (_ : ¬(a ≃ 0 ∧ Nonzero a))) :=
  zero? a
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ Nonzero a ↔ a ≄ 0

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ Nonzero a ↔ a ≄ 0
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ Nonzero a → a ≄ 0

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ a ≄ 0 → Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ Nonzero a → a ≄ 0
Tactic:
case mp =>
  intro (_ : Nonzero a) (_ : a ≃ 0)
  show False
  have : a ≃ 0 ∧ Nonzero a := And.intro ‹a ≃ 0› ‹Nonzero a›
  exact absurd ‹a ≃ 0 ∧ Nonzero a› ‹¬(a ≃ 0 ∧ Nonzero a)›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ a ≄ 0 → Nonzero a
Tactic:
case mpr =>
  intro (_ : a ≄ 0)
  show Nonzero a
  match ‹a ≃ 0 ∨ Nonzero a› with
  | Or.inl (_ : a ≃ 0) =>
    exact absurd ‹a ≃ 0› ‹a ≄ 0›
  | Or.inr (_ : Nonzero a) =>
    exact ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ Nonzero a → a ≄ 0
Tactic:
intro (_ : Nonzero a) (_ : a ≃ 0)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝¹ : Nonzero a
x✝ : a ≃ 0
⊢ False

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝¹ : Nonzero a
x✝ : a ≃ 0
⊢ False
Tactic:
have : a ≃ 0 ∧ Nonzero a := And.intro ‹a ≃ 0› ‹Nonzero a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝¹ : Nonzero a
x✝ : a ≃ 0
this : a ≃ 0 ∧ Nonzero a
⊢ False

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝¹ : Nonzero a
x✝ : a ≃ 0
this : a ≃ 0 ∧ Nonzero a
⊢ False
Tactic:
exact absurd ‹a ≃ 0 ∧ Nonzero a› ‹¬(a ≃ 0 ∧ Nonzero a)›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
⊢ a ≄ 0 → Nonzero a
Tactic:
intro (_ : a ≄ 0)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝ : a ≄ 0
⊢ Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝ : a ≄ 0
⊢ Nonzero a
Tactic:
match ‹a ≃ 0 ∨ Nonzero a› with
| Or.inl (_ : a ≃ 0) =>
  exact absurd ‹a ≃ 0› ‹a ≄ 0›
| Or.inr (_ : Nonzero a) =>
  exact ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝ : a ≄ 0
h✝ : a ≃ 0
⊢ Nonzero a
Tactic:
exact absurd ‹a ≃ 0› ‹a ≄ 0›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : a ≃ 0 ∨ Nonzero a
right✝ : ¬(a ≃ 0 ∧ Nonzero a)
x✝ : a ≄ 0
h✝ : Nonzero a
⊢ Nonzero a
Tactic:
exact ‹Nonzero a›
State after:
no goals