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

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
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

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›
State after:
no goals

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›
State after:
no goals

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)
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

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
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

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
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

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›
State after:
no goals

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)
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

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›
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

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›
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

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›
State after:
no goals

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
State after:
no goals

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›)
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

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›
State after:
no goals

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
State after:
no goals

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›
State after:
no goals

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
State after:
no goals

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›)
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

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›
State after:
no goals