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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 1 ↔ Sqrt1 b ∧ 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 : ℤ
⊢ a * b ≃ 1 → Sqrt1 b ∧ a ≃ b

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ 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 : ℤ
⊢ a * b ≃ 1 → Sqrt1 b ∧ a ≃ b
Tactic:
case mp =>
  intro (_ : a * b ≃ 1)
  show Sqrt1 b ∧ a ≃ b
  have : (a * b) * (a * b) ≃ 1 := calc
    (a * b) * (a * b) ≃ _ := AA.substL ‹a * b ≃ 1›
    1 * (a * b)       ≃ _ := AA.identL
    a * b             ≃ _ := ‹a * b ≃ 1›
    1                 ≃ _ := Rel.refl
  have : Sqrt1 (a * b) := Sqrt1.mk this
  have (And.intro (_ : Sqrt1 a) (_ : Sqrt1 b)) :=
    sqrt1_factors_if_sqrt1_product this
  have : b ≃ 1 ∨ b ≃ -1 := sqrt1_cases.mp ‹Sqrt1 b›
  have : a ≃ b :=
    match this with
    | Or.inl (_ : b ≃ 1) => calc
      a     ≃ _ := Rel.symm AA.identR
      a * 1 ≃ _ := AA.substR (Rel.symm ‹b ≃ 1›)
      a * b ≃ _ := ‹a * b ≃ 1›
      1     ≃ _ := Rel.symm ‹b ≃ 1›
      b     ≃ _ := Rel.refl
    | Or.inr (_ : b ≃ -1) => calc
      a             ≃ _ := Rel.symm neg_involutive
      (-(-a))       ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
      (-(-(a * 1))) ≃ _ := AA.subst₁ AA.scompatR
      (-(a * -1))   ≃ _ := AA.subst₁ (AA.substR (Rel.symm ‹b ≃ -1›))
      (-(a * b))    ≃ _ := AA.subst₁ ‹a * b ≃ 1›
      (-1)          ≃ _ := Rel.symm ‹b ≃ -1›
      b             ≃ _ := Rel.refl
  exact And.intro ‹Sqrt1 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 : ℤ
⊢ Sqrt1 b ∧ a ≃ b → a * b ≃ 1
Tactic:
case mpr =>
  intro (And.intro (_ : Sqrt1 b) (_ : a ≃ b))
  show a * b ≃ 1
  calc
    a * b ≃ _ := AA.substL ‹a ≃ b›
    b * b ≃ _ := ‹Sqrt1 b›.elim
    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 : ℤ
⊢ a * b ≃ 1 → Sqrt1 b ∧ a ≃ b
Tactic:
intro (_ : a * b ≃ 1)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
have : (a * b) * (a * b) ≃ 1 := calc
  (a * b) * (a * b) ≃ _ := AA.substL ‹a * b ≃ 1›
  1 * (a * b)       ≃ _ := AA.identL
  a * b             ≃ _ := ‹a * b ≃ 1›
  1                 ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this : a * b * (a * b) ≃ 1
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this : a * b * (a * b) ≃ 1
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
have : Sqrt1 (a * b) := Sqrt1.mk this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝ : a * b * (a * b) ≃ 1
this : Sqrt1 (a * b)
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝ : a * b * (a * b) ≃ 1
this : Sqrt1 (a * b)
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
have (And.intro (_ : Sqrt1 a) (_ : Sqrt1 b)) :=
  sqrt1_factors_if_sqrt1_product this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝ : a * b * (a * b) ≃ 1
this : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝ : a * b * (a * b) ≃ 1
this : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
have : 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 : ℤ
x✝ : a * b ≃ 1
this✝¹ : a * b * (a * b) ≃ 1
this✝ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this : b ≃ 1 ∨ b ≃ -1
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝¹ : a * b * (a * b) ≃ 1
this✝ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this : b ≃ 1 ∨ b ≃ -1
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
have : a ≃ b :=
  match this with
  | Or.inl (_ : b ≃ 1) => calc
    a     ≃ _ := Rel.symm AA.identR
    a * 1 ≃ _ := AA.substR (Rel.symm ‹b ≃ 1›)
    a * b ≃ _ := ‹a * b ≃ 1›
    1     ≃ _ := Rel.symm ‹b ≃ 1›
    b     ≃ _ := Rel.refl
  | Or.inr (_ : b ≃ -1) => calc
    a             ≃ _ := Rel.symm neg_involutive
    (-(-a))       ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
    (-(-(a * 1))) ≃ _ := AA.subst₁ AA.scompatR
    (-(a * -1))   ≃ _ := AA.subst₁ (AA.substR (Rel.symm ‹b ≃ -1›))
    (-(a * b))    ≃ _ := AA.subst₁ ‹a * b ≃ 1›
    (-1)          ≃ _ := Rel.symm ‹b ≃ -1›
    b             ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝² : a * b * (a * b) ≃ 1
this✝¹ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this✝ : b ≃ 1 ∨ b ≃ -1
this : a ≃ b
⊢ Sqrt1 b ∧ a ≃ b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝² : a * b * (a * b) ≃ 1
this✝¹ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this✝ : b ≃ 1 ∨ b ≃ -1
this : a ≃ b
⊢ Sqrt1 b ∧ a ≃ b
Tactic:
exact And.intro ‹Sqrt1 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 : ℤ
⊢ Sqrt1 b ∧ a ≃ b → a * b ≃ 1
Tactic:
intro (And.intro (_ : Sqrt1 b) (_ : a ≃ b))
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
left✝ : Sqrt1 b
right✝ : a ≃ b
⊢ a * b ≃ 1

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
left✝ : Sqrt1 b
right✝ : a ≃ b
⊢ a * b ≃ 1
Tactic:
calc
  a * b ≃ _ := AA.substL ‹a ≃ b›
  b * b ≃ _ := ‹Sqrt1 b›.elim
  1     ≃ _ := Rel.refl
State after:
no goals