internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this : a₂ ≃ -1 * coe m
⊢ Negative a₂
Tactic:
have : NonzeroWithSign a₂ (-1) :=
  NonzeroWithSign.intro m ‹Positive m› ‹a₂ ≃ -1 * ↑m›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this✝ : a₂ ≃ -1 * coe m
this : NonzeroWithSign a₂ (-1)
⊢ Negative a₂
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this✝ : a₂ ≃ -1 * coe m
this : NonzeroWithSign a₂ (-1)
⊢ Negative a₂
Tactic:
have : Negative a₂ := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a₂ (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this✝¹ : a₂ ≃ -1 * coe m
this✝ : NonzeroWithSign a₂ (-1)
this : Negative a₂
⊢ Negative a₂
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this✝¹ : a₂ ≃ -1 * coe m
this✝ : NonzeroWithSign a₂ (-1)
this : Negative a₂
⊢ Negative a₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_one_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
⊢ Negative (-1)
Tactic:
have : Positive (1:ℕ) := Natural.one_positive
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : Positive 1
⊢ Negative (-1)
Theorem: Lean4Axiomatic.Integer.neg_one_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : Positive 1
⊢ Negative (-1)
Tactic:
have : (-1:ℤ) ≃ -(coe (1:ℕ)) := Rel.refl
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this✝ : Positive 1
this : -1 ≃ -coe 1
⊢ Negative (-1)
Theorem: Lean4Axiomatic.Integer.neg_one_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this✝ : Positive 1
this : -1 ≃ -coe 1
⊢ Negative (-1)
Tactic:
have : Negative (-1:ℤ) :=
  negative_intro_nat ‹Positive (1:ℕ)› ‹(-1:ℤ) ≃ -(coe (1:ℕ))›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this✝¹ : Positive 1
this✝ : -1 ≃ -coe 1
this : Negative (-1)
⊢ Negative (-1)
Theorem: Lean4Axiomatic.Integer.neg_one_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this✝¹ : Positive 1
this✝ : -1 ≃ -coe 1
this : Negative (-1)
⊢ Negative (-1)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.not_positive_and_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ ¬(Positive a ∧ Negative a)
Tactic:
intro (And.intro (_ : Positive a) (_ : Negative a))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
⊢ False
Theorem: Lean4Axiomatic.Integer.not_positive_and_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
⊢ False
Tactic:
have two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a) :=
  AA.TwoOfThree.twoAndThree ‹Positive a› ‹Negative a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Theorem: Lean4Axiomatic.Integer.not_positive_and_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Tactic:
have not_two : ¬ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a) :=
  (sign_trichotomy a).atMostOne
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
not_two : ¬AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Theorem: Lean4Axiomatic.Integer.not_positive_and_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
not_two : ¬AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Tactic:
exact absurd two not_two
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a ↔ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ a ≃ 1 ∨ a ≃ -1 → Sqrt1 a
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1
Tactic:
case mp =>
  intro (_ : Sqrt1 a)
  show a ≃ 1 ∨ a ≃ -1
  match (sign_trichotomy a).atLeastOne with
  | AA.OneOfThree.first (_ : a ≃ 0) =>
    apply False.elim
    show False
    have : (1 : ℤ) ≃ 0 := calc
      1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
      a * a ≃ _ := AA.substL ‹a ≃ 0›
      0 * a ≃ _ := AA.absorbL
      0     ≃ _ := Rel.refl
    exact absurd ‹(1 : ℤ) ≃ 0› one_neqv_zero
  | AA.OneOfThree.second (_ : Positive a) =>
    apply Or.inl
    show a ≃ 1
    have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
      positive_elim_nat ‹Positive a›
    have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
      ((n * n : ℕ) : ℤ) ≃ _ := AA.compat₂
      (n : ℤ) * (n : ℤ) ≃ _ := AA.substL (Rel.symm ‹a ≃ (n : ℤ)›)
      a * (n : ℤ)       ≃ _ := AA.substR (Rel.symm ‹a ≃ (n : ℤ)›)
      a * a             ≃ _ := ‹Sqrt1 a›.elim
      1                 ≃ _ := Rel.refl
    have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
    have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
    show a ≃ 1
    calc
      a       ≃ _ := ‹a ≃ (n : ℤ)›
      (n : ℤ) ≃ _ := AA.subst₁ ‹n ≃ 1›
      (1 : ℤ) ≃ _ := Rel.refl
      (1 : ℤ) ≃ _ := Rel.refl
  | AA.OneOfThree.third (_ : Negative a) =>
    apply Or.inr
    show a ≃ -1
    have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ -(n : ℤ)))) :=
      negative_elim_nat ‹Negative a›
    have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
      ((n * n : ℕ) : ℤ)         ≃ _ := AA.compat₂
      (n : ℤ) * (n : ℤ)         ≃ _ := Rel.symm neg_involutive
      (-(-((n : ℤ) * (n : ℤ)))) ≃ _ := AA.subst₁ AA.scompatR
      (-((n : ℤ) * -(n : ℤ)))   ≃ _ := AA.scompatL
      (-(n : ℤ)) * (-(n : ℤ))   ≃ _ := AA.substL (Rel.symm ‹a ≃ -(n : ℤ)›)
      a * (-(n : ℤ))            ≃ _ := AA.substR (Rel.symm ‹a ≃ -(n : ℤ)›)
      a * a                     ≃ _ := ‹Sqrt1 a›.elim
      1                         ≃ _ := Rel.refl
    have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
    have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
    show a ≃ -1
    calc
      a          ≃ _ := ‹a ≃ -(n : ℤ)›
      (-(n : ℤ)) ≃ _ := AA.subst₁ (AA.subst₁ ‹n ≃ 1›)
      (-(1 : ℤ)) ≃ _ := Rel.refl
      (-1)       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ a ≃ 1 ∨ a ≃ -1 → Sqrt1 a
Tactic:
case mpr =>
  intro (_ : a ≃ 1 ∨ a ≃ -1)
  show Sqrt1 a
  match ‹a ≃ 1 ∨ a ≃ -1› with
  | Or.inl (_ : a ≃ 1) =>
    have : Sqrt1 (1 : ℤ) := sqrt1_one
    have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
    exact this
  | Or.inr (_ : a ≃ -1) =>
    have : Sqrt1 (-1 : ℤ) := sqrt1_neg_one
    have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ -1›) ‹Sqrt1 (-1 : ℤ)›
    exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1
Tactic:
intro (_ : Sqrt1 a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
⊢ a ≃ 1 ∨ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
match (sign_trichotomy a).atLeastOne with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  apply False.elim
  show False
  have : (1 : ℤ) ≃ 0 := calc
    1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
    a * a ≃ _ := AA.substL ‹a ≃ 0›
    0 * a ≃ _ := AA.absorbL
    0     ≃ _ := Rel.refl
  exact absurd ‹(1 : ℤ) ≃ 0› one_neqv_zero
| AA.OneOfThree.second (_ : Positive a) =>
  apply Or.inl
  show a ≃ 1
  have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
    positive_elim_nat ‹Positive a›
  have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
    ((n * n : ℕ) : ℤ) ≃ _ := AA.compat₂
    (n : ℤ) * (n : ℤ) ≃ _ := AA.substL (Rel.symm ‹a ≃ (n : ℤ)›)
    a * (n : ℤ)       ≃ _ := AA.substR (Rel.symm ‹a ≃ (n : ℤ)›)
    a * a             ≃ _ := ‹Sqrt1 a›.elim
    1                 ≃ _ := Rel.refl
  have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
  have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
  show a ≃ 1
  calc
    a       ≃ _ := ‹a ≃ (n : ℤ)›
    (n : ℤ) ≃ _ := AA.subst₁ ‹n ≃ 1›
    (1 : ℤ) ≃ _ := Rel.refl
    (1 : ℤ) ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a) =>
  apply Or.inr
  show a ≃ -1
  have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ -(n : ℤ)))) :=
    negative_elim_nat ‹Negative a›
  have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
    ((n * n : ℕ) : ℤ)         ≃ _ := AA.compat₂
    (n : ℤ) * (n : ℤ)         ≃ _ := Rel.symm neg_involutive
    (-(-((n : ℤ) * (n : ℤ)))) ≃ _ := AA.subst₁ AA.scompatR
    (-((n : ℤ) * -(n : ℤ)))   ≃ _ := AA.scompatL
    (-(n : ℤ)) * (-(n : ℤ))   ≃ _ := AA.substL (Rel.symm ‹a ≃ -(n : ℤ)›)
    a * (-(n : ℤ))            ≃ _ := AA.substR (Rel.symm ‹a ≃ -(n : ℤ)›)
    a * a                     ≃ _ := ‹Sqrt1 a›.elim
    1                         ≃ _ := Rel.refl
  have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
  have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
  show a ≃ -1
  calc
    a          ≃ _ := ‹a ≃ -(n : ℤ)›
    (-(n : ℤ)) ≃ _ := AA.subst₁ (AA.subst₁ ‹n ≃ 1›)
    (-(1 : ℤ)) ≃ _ := Rel.refl
    (-1)       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply False.elim
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ False
Tactic:
have : (1 : ℤ) ≃ 0 := calc
  1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
  a * a ≃ _ := AA.substL ‹a ≃ 0›
  0 * a ≃ _ := AA.absorbL
  0     ≃ _ := Rel.refl
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
this : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
this : 1 ≃ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℤ) ≃ 0› one_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Or.inl
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1
Tactic:
have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
  positive_elim_nat ‹Positive a›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
⊢ a ≃ 1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
⊢ a ≃ 1
Tactic:
have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
  ((n * n : ℕ) : ℤ) ≃ _ := AA.compat₂
  (n : ℤ) * (n : ℤ) ≃ _ := AA.substL (Rel.symm ‹a ≃ (n : ℤ)›)
  a * (n : ℤ)       ≃ _ := AA.substR (Rel.symm ‹a ≃ (n : ℤ)›)
  a * a             ≃ _ := ‹Sqrt1 a›.elim
  1                 ≃ _ := Rel.refl
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this : coe (n * n) ≃ 1
⊢ a ≃ 1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this : coe (n * n) ≃ 1
⊢ a ≃ 1
Tactic:
have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ 1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ 1
Tactic:
have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ 1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ 1
Tactic:
calc
  a       ≃ _ := ‹a ≃ (n : ℤ)›
  (n : ℤ) ≃ _ := AA.subst₁ ‹n ≃ 1›
  (1 : ℤ) ≃ _ := Rel.refl
  (1 : ℤ) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Or.inr
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ -1
Tactic:
have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ -(n : ℤ)))) :=
  negative_elim_nat ‹Negative a›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
⊢ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
⊢ a ≃ -1
Tactic:
have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
  ((n * n : ℕ) : ℤ)         ≃ _ := AA.compat₂
  (n : ℤ) * (n : ℤ)         ≃ _ := Rel.symm neg_involutive
  (-(-((n : ℤ) * (n : ℤ)))) ≃ _ := AA.subst₁ AA.scompatR
  (-((n : ℤ) * -(n : ℤ)))   ≃ _ := AA.scompatL
  (-(n : ℤ)) * (-(n : ℤ))   ≃ _ := AA.substL (Rel.symm ‹a ≃ -(n : ℤ)›)
  a * (-(n : ℤ))            ≃ _ := AA.substR (Rel.symm ‹a ≃ -(n : ℤ)›)
  a * a                     ≃ _ := ‹Sqrt1 a›.elim
  1                         ≃ _ := Rel.refl
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this : coe (n * n) ≃ 1
⊢ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this : coe (n * n) ≃ 1
⊢ a ≃ -1
Tactic:
have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ -1
Tactic:
have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ -1
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ -1
Tactic:
calc
  a          ≃ _ := ‹a ≃ -(n : ℤ)›
  (-(n : ℤ)) ≃ _ := AA.subst₁ (AA.subst₁ ‹n ≃ 1›)
  (-(1 : ℤ)) ≃ _ := Rel.refl
  (-1)       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ a ≃ 1 ∨ a ≃ -1 → Sqrt1 a
Tactic:
intro (_ : a ≃ 1 ∨ a ≃ -1)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
⊢ Sqrt1 a
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
⊢ Sqrt1 a
Tactic:
match ‹a ≃ 1 ∨ a ≃ -1› with
| Or.inl (_ : a ≃ 1) =>
  have : Sqrt1 (1 : ℤ) := sqrt1_one
  have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
  exact this
| Or.inr (_ : a ≃ -1) =>
  have : Sqrt1 (-1 : ℤ) := sqrt1_neg_one
  have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ -1›) ‹Sqrt1 (-1 : ℤ)›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
⊢ Sqrt1 a
Tactic:
have : Sqrt1 (1 : ℤ) := sqrt1_one
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this : Sqrt1 1
⊢ Sqrt1 a
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this : Sqrt1 1
⊢ Sqrt1 a
Tactic:
have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this✝ : Sqrt1 1
this : Sqrt1 a
⊢ Sqrt1 a
Theorem: Lean4Axiomatic.Integer.sqrt1_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this✝ : Sqrt1 1
this : Sqrt1 a
⊢ Sqrt1 a
Tactic:
exact this
Proof state after:
no goals