internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this✝ : Positive n
this : Positive (coe n)
⊢ Nonzero (coe n)
Tactic:
have : Nonzero (n : ℤ) := nonzero_from_positive this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this✝¹ : Positive n
this✝ : Positive (coe n)
this : Nonzero (coe n)
⊢ Nonzero (coe n)
Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this✝¹ : Positive n
this✝ : Positive (coe n)
this : Nonzero (coe n)
⊢ Nonzero (coe n)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)
Tactic:
have tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a) :=
  Signed.trichotomy a
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)
Tactic:
apply And.intro
Proof state after:
case left
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a

case right
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
case left =>
  show a ≃ 0 ∨ Nonzero a
  match tri.atLeastOne with
  | AA.OneOfThree.first (_ : a ≃ 0) =>
    exact Or.inl ‹a ≃ 0›
  | AA.OneOfThree.second (_ : Positive a) =>
    have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
    exact Or.inr ‹Nonzero a›
  | AA.OneOfThree.third (_ : Negative a) =>
    have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
    exact Or.inr ‹Nonzero a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)
Tactic:
case right =>
  intro (And.intro (_ : a ≃ 0) (_ : Nonzero a))
  show False
  apply tri.atMostOne
  show AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  match ‹Positive a ∨ Negative a› with
  | Or.inl (_ : Positive a) =>
    exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
  | Or.inr (_ : Negative a) =>
    exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
match tri.atLeastOne with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  exact Or.inl ‹a ≃ 0›
| AA.OneOfThree.second (_ : Positive a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
  exact Or.inr ‹Nonzero a›
| AA.OneOfThree.third (_ : Negative a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
  exact Or.inr ‹Nonzero a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inl ‹a ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inr ‹Nonzero a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inr ‹Nonzero a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)
Tactic:
intro (And.intro (_ : a ≃ 0) (_ : Nonzero a))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ False
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ False
Tactic:
apply tri.atMostOne
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
match ‹Positive a ∨ Negative a› with
| Or.inl (_ : Positive a) =>
  exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
| Or.inr (_ : Negative a) =>
  exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Positive a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero?
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_neqv_zero
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 0 ↔ a ≃ 0 ∨ b ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 0 → a ≃ 0 ∨ b ≃ 0

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a ≃ 0 ∨ b ≃ 0 → a * b ≃ 0
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a ≃ 0 ∨ b ≃ 0 → a * b ≃ 0
Tactic:
case mpr =>
  intro (_ : a ≃ 0 ∨ b ≃ 0)
  show a * b ≃ 0
  match ‹a ≃ 0 ∨ b ≃ 0› with
  | Or.inl (_ : a ≃ 0) => calc
    a * b ≃ _ := AA.substL ‹a ≃ 0›
    0 * b ≃ _ := AA.absorbL
    0     ≃ _ := Rel.refl
  | Or.inr (_ : b ≃ 0) => calc
    a * b ≃ _ := AA.substR ‹b ≃ 0›
    a * 0 ≃ _ := AA.absorbR
    0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 0 → a ≃ 0 ∨ b ≃ 0
Tactic:
intro (_ : a * b ≃ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
⊢ a ≃ 0 ∨ b ≃ 0
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
⊢ a ≃ 0 ∨ b ≃ 0
Tactic:
have : a ≃ 0 ∨ Nonzero a := (zero? a).left
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this : a ≃ 0 ∨ Nonzero a
⊢ a ≃ 0 ∨ b ≃ 0
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this : a ≃ 0 ∨ Nonzero a
h✝ : a ≃ 0
⊢ a ≃ 0 ∨ b ≃ 0
Tactic:
exact Or.inl ‹a ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this : a ≃ 0 ∨ Nonzero a
h✝ : Nonzero a
⊢ a ≃ 0 ∨ b ≃ 0
Tactic:
have : b ≃ 0 ∨ Nonzero b := (zero? b).left
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝ : a ≃ 0 ∨ Nonzero a
h✝ : Nonzero a
this : b ≃ 0 ∨ Nonzero b
⊢ a ≃ 0 ∨ b ≃ 0
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this : b ≃ 0 ∨ Nonzero b
h✝ : b ≃ 0
⊢ a ≃ 0 ∨ b ≃ 0
Tactic:
exact Or.inr ‹b ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
⊢ a ≃ 0 ∨ b ≃ 0
Tactic:
apply False.elim
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
⊢ False
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
⊢ False
Tactic:
have : ¬ (a * b ≃ 0 ∧ Nonzero (a * b)) := (zero? (a * b)).right
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ False
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ False
Tactic:
apply this
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ a * b ≃ 0 ∧ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ a * b ≃ 0 ∧ Nonzero (a * b)
Tactic:
apply And.intro
Proof state after:
case h.left
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ a * b ≃ 0

case h.right
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
case h.left
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ a * b ≃ 0
Tactic:
exact ‹a * b ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
case h.right
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ Nonzero (a * b)
Tactic:
exact mul_preserves_nonzero ‹Nonzero a› ‹Nonzero b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a ≃ 0 ∨ b ≃ 0 → a * b ≃ 0
Tactic:
intro (_ : a ≃ 0 ∨ b ≃ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a ≃ 0 ∨ b ≃ 0
⊢ a * b ≃ 0