internlm/Lean-Github huggingface dataset:
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_neg_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
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a * b ≃ -1 ↔ a ≄ b
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 : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a * b ≃ -1 → a ≄ b

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a ≄ b → a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a * b ≃ -1 → a ≄ b
Tactic:
case mp =>
  intro (_ : a * b ≃ -1) (_ : a ≃ b)
  show False
  have : (-1 : ℤ) ≃ 1 := calc
    (-1 : ℤ) ≃ _ := Rel.symm ‹a * b ≃ -1›
    a * b    ≃ _ := AA.substL ‹a ≃ b›
    b * b    ≃ _ := ‹Sqrt1 b›.elim
    1        ≃ _ := Rel.refl
  have : (-1 : ℤ) ≄ 1 := neg_one_neqv_one
  exact absurd ‹(-1 : ℤ) ≃ 1› ‹(-1 : ℤ) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a ≄ b → a * b ≃ -1
Tactic:
case mpr =>
  intro (_ : a ≄ b)
  show a * b ≃ -1
  have a_cases : a ≃ 1 ∨ a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 a›
  have b_cases : b ≃ 1 ∨ b ≃ -1 := sqrt1_cases.mp ‹Sqrt1 b›
  match a_cases with
  | Or.inl (_ : a ≃ 1) =>
    match b_cases with
    | Or.inl (_ : b ≃ 1) =>
      have : a ≃ b := Rel.trans ‹a ≃ 1› (Rel.symm ‹b ≃ 1›)
      exact absurd ‹a ≃ b› ‹a ≄ b›
    | Or.inr (_ : b ≃ -1) =>
      calc
        a * b ≃ _ := AA.substL ‹a ≃ 1›
        1 * b ≃ _ := AA.identL
        b     ≃ _ := ‹b ≃ -1›
        (-1)  ≃ _ := Rel.refl
  | Or.inr (_ : a ≃ -1) =>
    match b_cases with
    | Or.inl (_ : b ≃ 1) =>
      calc
        a * b ≃ _ := AA.substR ‹b ≃ 1›
        a * 1 ≃ _ := AA.identR
        a     ≃ _ := ‹a ≃ -1›
        (-1)  ≃ _ := Rel.refl
    | Or.inr (_ : b ≃ -1) =>
      have : a ≃ b := Rel.trans ‹a ≃ -1› (Rel.symm ‹b ≃ -1›)
      exact absurd ‹a ≃ b› ‹a ≄ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a * b ≃ -1 → a ≄ b
Tactic:
intro (_ : a * b ≃ -1) (_ : a ≃ b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
⊢ False
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
⊢ False
Tactic:
have : (-1 : ℤ) ≃ 1 := calc
  (-1 : ℤ) ≃ _ := Rel.symm ‹a * b ≃ -1›
  a * b    ≃ _ := AA.substL ‹a ≃ b›
  b * b    ≃ _ := ‹Sqrt1 b›.elim
  1        ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
this : -1 ≃ 1
⊢ False
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
this : -1 ≃ 1
⊢ False
Tactic:
have : (-1 : ℤ) ≄ 1 := neg_one_neqv_one
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
this✝ : -1 ≃ 1
this : -1 ≄ 1
⊢ False
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
this✝ : -1 ≃ 1
this : -1 ≄ 1
⊢ False
Tactic:
exact absurd ‹(-1 : ℤ) ≃ 1› ‹(-1 : ℤ) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a ≄ b → a * b ≃ -1
Tactic:
intro (_ : a ≄ b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
⊢ a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
⊢ a * b ≃ -1
Tactic:
have a_cases : a ≃ 1 ∨ a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 a›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
⊢ a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
⊢ a * b ≃ -1
Tactic:
have b_cases : b ≃ 1 ∨ b ≃ -1 := sqrt1_cases.mp ‹Sqrt1 b›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
⊢ a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
⊢ a * b ≃ -1
Tactic:
match a_cases with
| Or.inl (_ : a ≃ 1) =>
  match b_cases with
  | Or.inl (_ : b ≃ 1) =>
    have : a ≃ b := Rel.trans ‹a ≃ 1› (Rel.symm ‹b ≃ 1›)
    exact absurd ‹a ≃ b› ‹a ≄ b›
  | Or.inr (_ : b ≃ -1) =>
    calc
      a * b ≃ _ := AA.substL ‹a ≃ 1›
      1 * b ≃ _ := AA.identL
      b     ≃ _ := ‹b ≃ -1›
      (-1)  ≃ _ := Rel.refl
| Or.inr (_ : a ≃ -1) =>
  match b_cases with
  | Or.inl (_ : b ≃ 1) =>
    calc
      a * b ≃ _ := AA.substR ‹b ≃ 1›
      a * 1 ≃ _ := AA.identR
      a     ≃ _ := ‹a ≃ -1›
      (-1)  ≃ _ := Rel.refl
  | Or.inr (_ : b ≃ -1) =>
    have : a ≃ b := Rel.trans ‹a ≃ -1› (Rel.symm ‹b ≃ -1›)
    exact absurd ‹a ≃ b› ‹a ≄ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝ : a ≃ 1
⊢ a * b ≃ -1
Tactic:
match b_cases with
| Or.inl (_ : b ≃ 1) =>
  have : a ≃ b := Rel.trans ‹a ≃ 1› (Rel.symm ‹b ≃ 1›)
  exact absurd ‹a ≃ b› ‹a ≄ b›
| Or.inr (_ : b ≃ -1) =>
  calc
    a * b ≃ _ := AA.substL ‹a ≃ 1›
    1 * b ≃ _ := AA.identL
    b     ≃ _ := ‹b ≃ -1›
    (-1)  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ 1
h✝ : b ≃ 1
⊢ a * b ≃ -1
Tactic:
have : a ≃ b := Rel.trans ‹a ≃ 1› (Rel.symm ‹b ≃ 1›)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ 1
h✝ : b ≃ 1
this : a ≃ b
⊢ a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ 1
h✝ : b ≃ 1
this : a ≃ b
⊢ a * b ≃ -1
Tactic:
exact absurd ‹a ≃ b› ‹a ≄ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ 1
h✝ : b ≃ -1
⊢ a * b ≃ -1
Tactic:
calc
  a * b ≃ _ := AA.substL ‹a ≃ 1›
  1 * b ≃ _ := AA.identL
  b     ≃ _ := ‹b ≃ -1›
  (-1)  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝ : a ≃ -1
⊢ a * b ≃ -1
Tactic:
match b_cases with
| Or.inl (_ : b ≃ 1) =>
  calc
    a * b ≃ _ := AA.substR ‹b ≃ 1›
    a * 1 ≃ _ := AA.identR
    a     ≃ _ := ‹a ≃ -1›
    (-1)  ≃ _ := Rel.refl
| Or.inr (_ : b ≃ -1) =>
  have : a ≃ b := Rel.trans ‹a ≃ -1› (Rel.symm ‹b ≃ -1›)
  exact absurd ‹a ≃ b› ‹a ≄ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ -1
h✝ : b ≃ 1
⊢ a * b ≃ -1
Tactic:
calc
  a * b ≃ _ := AA.substR ‹b ≃ 1›
  a * 1 ≃ _ := AA.identR
  a     ≃ _ := ‹a ≃ -1›
  (-1)  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ -1
h✝ : b ≃ -1
⊢ a * b ≃ -1
Tactic:
have : a ≃ b := Rel.trans ‹a ≃ -1› (Rel.symm ‹b ≃ -1›)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ -1
h✝ : b ≃ -1
this : a ≃ b
⊢ a * b ≃ -1
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_neqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ -1
h✝ : b ≃ -1
this : a ≃ b
⊢ a * b ≃ -1
Tactic:
exact absurd ‹a ≃ b› ‹a ≄ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
⊢ NonzeroWithSign a s → NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
intro (_ : NonzeroWithSign a s)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
have : s ≃ 1 ∨ s ≃ -1 := sqrt1_cases.mp ‹Sqrt1 s›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this : s ≃ 1 ∨ s ≃ -1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this : s ≃ 1 ∨ s ≃ -1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
match ‹s ≃ 1 ∨ s ≃ -1› with
| Or.inl (_ : s ≃ 1) =>
  have : NonzeroWithSign a 1 :=
    NonzeroWithSign.subst_sign ‹s ≃ 1› ‹NonzeroWithSign a s›
  exact Or.inl ‹NonzeroWithSign a 1›
| Or.inr (_ : s ≃ -1) =>
  have : NonzeroWithSign a (-1) :=
    NonzeroWithSign.subst_sign ‹s ≃ -1› ‹NonzeroWithSign a s›
  exact Or.inr ‹NonzeroWithSign a (-1)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ 1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
have : NonzeroWithSign a 1 :=
  NonzeroWithSign.subst_sign ‹s ≃ 1› ‹NonzeroWithSign a s›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this✝ : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ 1
this : NonzeroWithSign a 1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this✝ : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ 1
this : NonzeroWithSign a 1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
exact Or.inl ‹NonzeroWithSign a 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ -1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
have : NonzeroWithSign a (-1) :=
  NonzeroWithSign.subst_sign ‹s ≃ -1› ‹NonzeroWithSign a s›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this✝ : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ -1
this : NonzeroWithSign a (-1)
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_cases
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this✝ : s ≃ 1 ∨ s ≃ -1
h✝ : s ≃ -1
this : NonzeroWithSign a (-1)
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
Tactic:
exact Or.inr ‹NonzeroWithSign a (-1)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝¹ : Sqrt1 s₁
x✝ : Sqrt1 s₂
⊢ NonzeroWithSign a s₁ → NonzeroWithSign a s₂ → s₁ ≃ s₂
Tactic:
intro (_ : NonzeroWithSign a s₁) (_ : NonzeroWithSign a s₂)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
⊢ s₁ ≃ s₂
Tactic:
have : s₁ ≃ 1 ∨ s₁ ≃ -1 := sqrt1_cases.mp ‹Sqrt1 s₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this : s₁ ≃ 1 ∨ s₁ ≃ -1
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this : s₁ ≃ 1 ∨ s₁ ≃ -1
⊢ s₁ ≃ s₂
Tactic:
have : s₂ ≃ 1 ∨ s₂ ≃ -1 := sqrt1_cases.mp ‹Sqrt1 s₂›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝ : s₁ ≃ 1 ∨ s₁ ≃ -1
this : s₂ ≃ 1 ∨ s₂ ≃ -1
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝ : s₁ ≃ 1 ∨ s₁ ≃ -1
this : s₂ ≃ 1 ∨ s₂ ≃ -1
⊢ s₁ ≃ s₂
Tactic:
have : s₁ ≃ s₂ ∨ (NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)) :=
  match ‹s₁ ≃ 1 ∨ s₁ ≃ -1› with
  | Or.inl (_ : s₁ ≃ 1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ 1› (Rel.symm ‹s₂ ≃ 1›)
      Or.inl ‹s₁ ≃ s₂›
    | Or.inr (_ : s₂ ≃ -1) =>
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ 1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ -1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
  | Or.inr (_ : s₁ ≃ -1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ -1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ 1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
    | Or.inr (_ : s₂ ≃ -1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ -1› (Rel.symm ‹s₂ ≃ -1›)
      Or.inl ‹s₁ ≃ s₂›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
Tactic:
match this with
| Or.inl (_ : s₁ ≃ s₂) =>
  exact ‹s₁ ≃ s₂›
| Or.inr (And.intro (_ : NonzeroWithSign a 1) (_ : NonzeroWithSign a (-1))) =>
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  have : Positive a ∧ Negative a := And.intro ‹Positive a› ‹Negative a›
  exact absurd ‹Positive a ∧ Negative a› not_positive_and_negative
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
h✝ : s₁ ≃ s₂
⊢ s₁ ≃ s₂
Tactic:
exact ‹s₁ ≃ s₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
Tactic:
have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝² : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝¹ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this : Positive a
⊢ s₁ ≃ s₂