[GOAL]
R : Type u_1
c₁ c₂ : R
f : Fin 4 → R
⊢ (fun a => ![a.re, a.imI, a.imJ, a.imK]) ((fun a => { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) f) = f
[PROOFSTEP]
ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩
[GOAL]
case h.mk.refl
R : Type u_1
c₁ c₂ : R
f : Fin 4 → R
⊢ (fun a => ![a.re, a.imI, a.imJ, a.imK]) ((fun a => { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) f)
      { val := 3, isLt := (_ : Nat.le (Nat.succ 3) (Nat.succ 3)) } =
    f { val := 3, isLt := (_ : Nat.le (Nat.succ 3) (Nat.succ 3)) }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.step.refl
R : Type u_1
c₁ c₂ : R
f : Fin 4 → R
⊢ (fun a => ![a.re, a.imI, a.imJ, a.imK]) ((fun a => { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) f)
      { val := 2, isLt := (_ : Nat.le (Nat.succ 2) (Nat.succ 3)) } =
    f { val := 2, isLt := (_ : Nat.le (Nat.succ 2) (Nat.succ 3)) }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.step.step.refl
R : Type u_1
c₁ c₂ : R
f : Fin 4 → R
⊢ (fun a => ![a.re, a.imI, a.imJ, a.imK]) ((fun a => { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) f)
      { val := 1, isLt := (_ : Nat.le (Nat.succ 1) (Nat.succ 3)) } =
    f { val := 1, isLt := (_ : Nat.le (Nat.succ 1) (Nat.succ 3)) }
[PROOFSTEP]
rfl
[GOAL]
case h.mk.step.step.step.refl
R : Type u_1
c₁ c₂ : R
f : Fin 4 → R
⊢ (fun a => ![a.re, a.imI, a.imJ, a.imK]) ((fun a => { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) f)
      { val := 0, isLt := (_ : Nat.le (Nat.succ 0) (Nat.succ 3)) } =
    f { val := 0, isLt := (_ : Nat.le (Nat.succ 0) (Nat.succ 3)) }
[PROOFSTEP]
rfl
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x + y)).re = (↑x + ↑y).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x + y)).imI = (↑x + ↑y).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x + y)).imJ = (↑x + ↑y).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x + y)).imK = (↑x + ↑y).imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ ↑(-x) = -↑x
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(-x)).re = (-↑x).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(-x)).imI = (-↑x).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(-x)).imJ = (-↑x).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(-x)).imK = (-↑x).imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝⁴ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ (s • t) • x = s • t • x
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝⁴ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ ((s • t) • x).re = (s • t • x).re
[PROOFSTEP]
exact smul_assoc _ _ _
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝⁴ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ ((s • t) • x).imI = (s • t • x).imI
[PROOFSTEP]
exact smul_assoc _ _ _
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝⁴ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ ((s • t) • x).imJ = (s • t • x).imJ
[PROOFSTEP]
exact smul_assoc _ _ _
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝⁴ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ ((s • t) • x).imK = (s • t • x).imK
[PROOFSTEP]
exact smul_assoc _ _ _
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝³ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ s • t • x = t • s • x
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝³ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ (s • t • x).re = (t • s • x).re
[PROOFSTEP]
exact smul_comm _ _ _
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝³ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ (s • t • x).imI = (t • s • x).imI
[PROOFSTEP]
exact smul_comm _ _ _
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝³ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ (s • t • x).imJ = (t • s • x).imJ
[PROOFSTEP]
exact smul_comm _ _ _
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝³ : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂]
⊢ (s • t • x).imK = (t • s • x).imK
[PROOFSTEP]
exact smul_comm _ _ _
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
change coe _ = -coe _
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑↑(n + 1)
[PROOFSTEP]
rw [Int.cast_negSucc, coe_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * x✝).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * (x✝¹ + x✝)).imI = (x✝² * x✝¹ + x✝² * x✝).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * (x✝¹ + x✝)).imJ = (x✝² * x✝¹ + x✝² * x✝).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * (x✝¹ + x✝)).imK = (x✝² * x✝¹ + x✝² * x✝).imK
[PROOFSTEP]
simp
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝².re * (x✝¹.re + x✝.re) + c₁ * x✝².imI * (x✝¹.imI + x✝.imI) + c₂ * x✝².imJ * (x✝¹.imJ + x✝.imJ) -
      c₁ * c₂ * x✝².imK * (x✝¹.imK + x✝.imK) =
    x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₂ * x✝².imJ * x✝¹.imJ - c₁ * c₂ * x✝².imK * x✝¹.imK +
      (x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₂ * x✝².imJ * x✝.imJ - c₁ * c₂ * x✝².imK * x✝.imK)
[PROOFSTEP]
ring
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝².re * (x✝¹.imI + x✝.imI) + x✝².imI * (x✝¹.re + x✝.re) - c₂ * x✝².imJ * (x✝¹.imK + x✝.imK) +
      c₂ * x✝².imK * (x✝¹.imJ + x✝.imJ) =
    x✝².re * x✝¹.imI + x✝².imI * x✝¹.re - c₂ * x✝².imJ * x✝¹.imK + c₂ * x✝².imK * x✝¹.imJ +
      (x✝².re * x✝.imI + x✝².imI * x✝.re - c₂ * x✝².imJ * x✝.imK + c₂ * x✝².imK * x✝.imJ)
[PROOFSTEP]
ring
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝².re * (x✝¹.imJ + x✝.imJ) + c₁ * x✝².imI * (x✝¹.imK + x✝.imK) + x✝².imJ * (x✝¹.re + x✝.re) -
      c₁ * x✝².imK * (x✝¹.imI + x✝.imI) =
    x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re - c₁ * x✝².imK * x✝¹.imI +
      (x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re - c₁ * x✝².imK * x✝.imI)
[PROOFSTEP]
ring
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝².re * (x✝¹.imK + x✝.imK) + x✝².imI * (x✝¹.imJ + x✝.imJ) - x✝².imJ * (x✝¹.imI + x✝.imI) +
      x✝².imK * (x✝¹.re + x✝.re) =
    x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re +
      (x✝².re * x✝.imK + x✝².imI * x✝.imJ - x✝².imJ * x✝.imI + x✝².imK * x✝.re)
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ ((x✝² + x✝¹) * x✝).re = (x✝² * x✝ + x✝¹ * x✝).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ ((x✝² + x✝¹) * x✝).imI = (x✝² * x✝ + x✝¹ * x✝).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ ((x✝² + x✝¹) * x✝).imJ = (x✝² * x✝ + x✝¹ * x✝).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ ((x✝² + x✝¹) * x✝).imK = (x✝² * x✝ + x✝¹ * x✝).imK
[PROOFSTEP]
simp
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re + x✝¹.re) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imJ -
      c₁ * c₂ * (x✝².imK + x✝¹.imK) * x✝.imK =
    x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₂ * x✝².imJ * x✝.imJ - c₁ * c₂ * x✝².imK * x✝.imK +
      (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₂ * x✝¹.imJ * x✝.imJ - c₁ * c₂ * x✝¹.imK * x✝.imK)
[PROOFSTEP]
ring
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re + x✝¹.re) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re - c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₂ * (x✝².imK + x✝¹.imK) * x✝.imJ =
    x✝².re * x✝.imI + x✝².imI * x✝.re - c₂ * x✝².imJ * x✝.imK + c₂ * x✝².imK * x✝.imJ +
      (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₂ * x✝¹.imJ * x✝.imK + c₂ * x✝¹.imK * x✝.imJ)
[PROOFSTEP]
ring
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re + x✝¹.re) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re -
      c₁ * (x✝².imK + x✝¹.imK) * x✝.imI =
    x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re - c₁ * x✝².imK * x✝.imI +
      (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI)
[PROOFSTEP]
ring
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re + x✝¹.re) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ - (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ 0 * x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (0 * x✝).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (0 * x✝).imI = 0.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (0 * x✝).imJ = 0.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (0 * x✝).imK = 0.imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ x✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 0).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 0).imI = 0.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 0).imJ = 0.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 0).imK = 0.imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * x✝)).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * x✝¹ * x✝).imI = (x✝² * (x✝¹ * x✝)).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * x✝¹ * x✝).imJ = (x✝² * (x✝¹ * x✝)).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝² * x✝¹ * x✝).imK = (x✝² * (x✝¹ * x✝)).imK
[PROOFSTEP]
simp
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₂ * x✝².imJ * x✝¹.imJ - c₁ * c₂ * x✝².imK * x✝¹.imK) * x✝.re +
          c₁ * (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re - c₂ * x✝².imJ * x✝¹.imK + c₂ * x✝².imK * x✝¹.imJ) * x✝.imI +
        c₂ * (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re - c₁ * x✝².imK * x✝¹.imI) * x✝.imJ -
      c₁ * c₂ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.imK =
    x✝².re * (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₂ * x✝¹.imJ * x✝.imJ - c₁ * c₂ * x✝¹.imK * x✝.imK) +
          c₁ * x✝².imI * (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₂ * x✝¹.imJ * x✝.imK + c₂ * x✝¹.imK * x✝.imJ) +
        c₂ * x✝².imJ * (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI) -
      c₁ * c₂ * x✝².imK * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)
[PROOFSTEP]
ring
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₂ * x✝².imJ * x✝¹.imJ - c₁ * c₂ * x✝².imK * x✝¹.imK) * x✝.imI +
          (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re - c₂ * x✝².imJ * x✝¹.imK + c₂ * x✝².imK * x✝¹.imJ) * x✝.re -
        c₂ * (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re - c₁ * x✝².imK * x✝¹.imI) * x✝.imK +
      c₂ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.imJ =
    x✝².re * (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₂ * x✝¹.imJ * x✝.imK + c₂ * x✝¹.imK * x✝.imJ) +
          x✝².imI * (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₂ * x✝¹.imJ * x✝.imJ - c₁ * c₂ * x✝¹.imK * x✝.imK) -
        c₂ * x✝².imJ * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
      c₂ * x✝².imK * (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI)
[PROOFSTEP]
ring
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₂ * x✝².imJ * x✝¹.imJ - c₁ * c₂ * x✝².imK * x✝¹.imK) * x✝.imJ +
          c₁ * (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re - c₂ * x✝².imJ * x✝¹.imK + c₂ * x✝².imK * x✝¹.imJ) * x✝.imK +
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re - c₁ * x✝².imK * x✝¹.imI) * x✝.re -
      c₁ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.imI =
    x✝².re * (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI) +
          c₁ * x✝².imI * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
        x✝².imJ * (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₂ * x✝¹.imJ * x✝.imJ - c₁ * c₂ * x✝¹.imK * x✝.imK) -
      c₁ * x✝².imK * (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₂ * x✝¹.imJ * x✝.imK + c₂ * x✝¹.imK * x✝.imJ)
[PROOFSTEP]
ring
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₂ * x✝².imJ * x✝¹.imJ - c₁ * c₂ * x✝².imK * x✝¹.imK) * x✝.imK +
          (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re - c₂ * x✝².imJ * x✝¹.imK + c₂ * x✝².imK * x✝¹.imJ) * x✝.imJ -
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re - c₁ * x✝².imK * x✝¹.imI) * x✝.imI +
      (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.re =
    x✝².re * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
          x✝².imI * (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI) -
        x✝².imJ * (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₂ * x✝¹.imJ * x✝.imK + c₂ * x✝¹.imK * x✝.imJ) +
      x✝².imK * (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₂ * x✝¹.imJ * x✝.imJ - c₁ * c₂ * x✝¹.imK * x✝.imK)
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ 1 * x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (1 * x✝).re = x✝.re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (1 * x✝).imI = x✝.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (1 * x✝).imJ = x✝.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (1 * x✝).imK = x✝.imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ x✝ * 1 = x✝
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 1).re = x✝.re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 1).imI = x✝.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 1).imJ = x✝.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : AddCommGroupWithOne ℍ[R,c₁,c₂] := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
x✝ : ℍ[R,c₁,c₂]
⊢ (x✝ * 1).imK = x✝.imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ ↑(x * y) = ↑x * ↑y
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x * y)).re = (↑x * ↑y).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x * y)).imI = (↑x * ↑y).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x * y)).imJ = (↑x * ↑y).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (↑(x * y)).imK = (↑x * ↑y).imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (fun s => ↑(↑(algebraMap S R) s)) 1 = 1
[PROOFSTEP]
simp only [map_one, coe_one]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y✝ z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ OneHom.toFun { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) } (x * y) =
    OneHom.toFun { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) } x *
      OneHom.toFun { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) } y
[PROOFSTEP]
simp only [map_mul, coe_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
          map_mul' :=
            (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) })
      0 =
    0
[PROOFSTEP]
simp only [map_zero, coe_zero]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y✝ z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
          map_mul' :=
            (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
            map_mul' :=
              (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
            map_mul' :=
              (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) })
        y
[PROOFSTEP]
simp only [map_add, coe_add]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                map_mul' :=
                  (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
            map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
            map_add' :=
              (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
        s *
      x =
    x *
      ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                map_mul' :=
                  (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
            map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
            map_add' :=
              (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
        s
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).re =
    (x *
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s).re
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imI =
    (x *
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s).imI
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imJ =
    (x *
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s).imJ
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imK =
    (x *
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s).imK
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ s • x =
    ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                map_mul' :=
                  (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
            map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
            map_add' :=
              (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
        s *
      x
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (s • x).re =
    (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).re
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (s • x).imI =
    (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imI
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (s • x).imJ =
    (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imJ
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁ c₂ r x✝ y z : R
a b c : ℍ[R,c₁,c₂]
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : (fun x => ℍ[R,c₁,c₂]) s
⊢ (s • x).imK =
    (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun s => ↑(↑(algebraMap S R) s), map_one' := (_ : ↑(↑(algebraMap S R) 1) = 1) },
                  map_mul' :=
                    (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x * y)) = ↑(↑(algebraMap S R) x) * ↑(↑(algebraMap S R) y)) },
              map_zero' := (_ : ↑(↑(algebraMap S R) 0) = 0),
              map_add' :=
                (_ : ∀ (x y : S), ↑(↑(algebraMap S R) (x + y)) = ↑(↑(algebraMap S R) x) + ↑(↑(algebraMap S R) y)) }
          s *
        x).imK
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝¹ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝ : StrongRankCondition R
⊢ Module.rank R ℍ[R,c₁,c₂] = 4
[PROOFSTEP]
rw [rank_eq_card_basis (basisOneIJK c₁ c₂), Fintype.card_fin]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝¹ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝ : StrongRankCondition R
⊢ ↑4 = 4
[PROOFSTEP]
norm_num
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝¹ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝ : StrongRankCondition R
⊢ FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4
[PROOFSTEP]
rw [FiniteDimensional.finrank, rank_eq_four, Cardinal.toNat_ofNat]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a * ↑r = r • a
[PROOFSTEP]
rw [← coe_commutes, coe_mul_eq_smul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ x • ↑y = ↑(x * y)
[PROOFSTEP]
rw [coe_mul, coe_mul_eq_smul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x✝ y z : R
a b c x : ℍ[R,c₁,c₂]
⊢ star (star x) = x
[PROOFSTEP]
simp [Star.star]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ star (a * b) = star b * star a
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a * b)).re = (star b * star a).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a * b)).imI = (star b * star a).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a * b)).imJ = (star b * star a).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a * b)).imK = (star b * star a).imK
[PROOFSTEP]
simp
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₂ * a.imJ * b.imJ - c₁ * c₂ * a.imK * b.imK =
    b.re * a.re + c₁ * b.imI * a.imI + c₂ * b.imJ * a.imJ - c₁ * c₂ * b.imK * a.imK
[PROOFSTEP]
ring
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ -(c₂ * a.imK * b.imJ) + (c₂ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re)) =
    -(b.re * a.imI) + -(b.imI * a.re) - c₂ * b.imJ * a.imK + c₂ * b.imK * a.imJ
[PROOFSTEP]
ring
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re) =
    -(b.re * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * a.re) - c₁ * b.imK * a.imI
[PROOFSTEP]
ring
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ)) =
    -(b.re * a.imK) + b.imI * a.imJ - b.imJ * a.imI + -(b.imK * a.re)
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ star (a + b) = star a + star b
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a + b)).re = (star a + star b).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a + b)).imI = (star a + star b).imI
[PROOFSTEP]
simp [add_comm]
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a + b)).imJ = (star a + star b).imJ
[PROOFSTEP]
simp [add_comm]
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a✝ b✝ c a b : ℍ[R,c₁,c₂]
⊢ (star (a + b)).imK = (star a + star b).imK
[PROOFSTEP]
simp [add_comm]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a + star a = ↑(2 * a.re)
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (a + star a).re = (↑(2 * a.re)).re
[PROOFSTEP]
simp [two_mul]
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (a + star a).imI = (↑(2 * a.re)).imI
[PROOFSTEP]
simp [two_mul]
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (a + star a).imJ = (↑(2 * a.re)).imJ
[PROOFSTEP]
simp [two_mul]
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (a + star a).imK = (↑(2 * a.re)).imK
[PROOFSTEP]
simp [two_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a + star a = 2 * ↑a.re
[PROOFSTEP]
simp only [self_add_star', two_mul, coe_add]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ star a + a = ↑(2 * a.re)
[PROOFSTEP]
rw [add_comm, self_add_star']
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ star a + a = 2 * ↑a.re
[PROOFSTEP]
rw [add_comm, self_add_star]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ Commute (star a) a
[PROOFSTEP]
rw [a.star_eq_two_re_sub]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ Commute (↑(2 * a.re) - a) a
[PROOFSTEP]
exact (coe_commute (2 * a.re) a).sub_left (Commute.refl a)
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ star ↑x = ↑x
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star ↑x).re = (↑x).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star ↑x).imI = (↑x).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star ↑x).imJ = (↑x).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star ↑x).imK = (↑x).imK
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x✝ y z : R
a✝ b c a : ℍ[R,c₁,c₂]
x : R
h : a = ↑x
⊢ a = ↑a.re
[PROOFSTEP]
rw [h, coe_re]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁✝ c₂✝ r x y z : R
a✝ b c : ℍ[R,c₁✝,c₂✝]
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂]
⊢ star a = a ↔ a = ↑a.re
[PROOFSTEP]
simp [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝² : CommRing R
c₁✝ c₂✝ r x y z : R
a✝ b c : ℍ[R,c₁✝,c₂✝]
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂]
⊢ star a = -a ↔ a.re = 0
[PROOFSTEP]
simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ star a * a = ↑(star a * a).re
[PROOFSTEP]
ext
[GOAL]
case re
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star a * a).re = (↑(star a * a).re).re
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star a * a).imI = (↑(star a * a).re).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star a * a).imJ = (↑(star a * a).re).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ (star a * a).imK = (↑(star a * a).re).imK
[PROOFSTEP]
simp
[GOAL]
case imI
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a.re * a.imI + -(a.imI * a.re) + c₂ * a.imJ * a.imK + -(c₂ * a.imK * a.imJ) = 0
[PROOFSTEP]
ring
[GOAL]
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a.re * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + c₁ * a.imK * a.imI = 0
[PROOFSTEP]
ring
[GOAL]
case imK
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a.re * a.imK + -(a.imI * a.imJ) + a.imJ * a.imI + -(a.imK * a.re) = 0
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ a * star a = ↑(a * star a).re
[PROOFSTEP]
rw [← star_comm_self']
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
⊢ star a * a = ↑(star a * a).re
[PROOFSTEP]
exact a.star_mul_eq_coe
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r x✝ y✝ z : R
a b c : ℍ[R,c₁,c₂]
src✝ : ℍ[R,c₁,c₂] ≃+ ℍ[R,c₁,c₂]ᵐᵒᵖ := AddEquiv.trans starAddEquiv opAddEquiv
x y : ℍ[R,c₁,c₂]
⊢ Equiv.toFun
      { toFun := op ∘ star, invFun := star ∘ unop, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (x * y) =
    Equiv.toFun
        { toFun := op ∘ star, invFun := star ∘ unop, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x *
      Equiv.toFun
        { toFun := op ∘ star, invFun := star ∘ unop, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
c₁ c₂ r✝ x y z : R
a b c : ℍ[R,c₁,c₂]
src✝ : ℍ[R,c₁,c₂] ≃+ ℍ[R,c₁,c₂]ᵐᵒᵖ := AddEquiv.trans starAddEquiv opAddEquiv
r : R
⊢ Equiv.toFun
      { toFun := op ∘ star, invFun := star ∘ unop, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R ℍ[R,c₁,c₂]) r) =
    ↑(algebraMap R ℍ[R,c₁,c₂]ᵐᵒᵖ) r
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ - -1 * -1 * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
[PROOFSTEP]
simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a.re * b.imI + a.imI * b.re - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ =
    a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ
[PROOFSTEP]
simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re - -1 * a.imK * b.imI =
    a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI
[PROOFSTEP]
simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
[PROOFSTEP]
simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ (fun a => (a * star a).re) 0 = 0
[PROOFSTEP]
simp only [star_zero, zero_mul, zero_re]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } 1 = 1
[PROOFSTEP]
simp only [star_one, one_mul, one_re]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ z : R
a b c x y : ℍ[R]
⊢ ↑(ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } (x * y)) =
    ↑(ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } x *
        ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } y)
[PROOFSTEP]
conv_lhs =>
  rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe, coe_commutes, ← mul_assoc,
    x.mul_star_eq_coe, ← coe_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ z : R
a b c x y : ℍ[R]
| ↑(ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } (x * y))
[PROOFSTEP]
rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe, coe_commutes, ← mul_assoc,
    x.mul_star_eq_coe, ← coe_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ z : R
a b c x y : ℍ[R]
| ↑(ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } (x * y))
[PROOFSTEP]
rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe, coe_commutes, ← mul_assoc,
    x.mul_star_eq_coe, ← coe_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ z : R
a b c x y : ℍ[R]
| ↑(ZeroHom.toFun { toFun := fun a => (a * star a).re, map_zero' := (_ : (0 * star 0).re = 0) } (x * y))
[PROOFSTEP]
rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe, coe_commutes, ← mul_assoc,
  x.mul_star_eq_coe, ← coe_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
[PROOFSTEP]
simp only [normSq_def, sq, mul_neg, sub_neg_eq_add, mul_re, star_re, star_imI, star_imJ, star_imK]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑normSq ↑x = x ^ 2
[PROOFSTEP]
rw [normSq_def, star_coe, ← coe_mul, coe_re, sq]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑normSq (star a) = ↑normSq a
[PROOFSTEP]
simp [normSq_def']
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
n : ℕ
⊢ ↑normSq ↑n = ↑n ^ 2
[PROOFSTEP]
rw [← coe_nat_cast, normSq_coe]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z✝ : R
a b c : ℍ[R]
z : ℤ
⊢ ↑normSq ↑z = ↑z ^ 2
[PROOFSTEP]
rw [← coe_int_cast, normSq_coe]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑normSq (-a) = ↑normSq a
[PROOFSTEP]
simp only [normSq_def, star_neg, neg_mul_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a * star a = ↑(↑normSq a)
[PROOFSTEP]
rw [mul_star_eq_coe, normSq_def]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ star a * a = ↑(↑normSq a)
[PROOFSTEP]
rw [star_comm_self, self_mul_star]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ im a ^ 2 = -↑(↑normSq (im a))
[PROOFSTEP]
simp_rw [sq, ← star_mul_self, im_star, neg_mul, neg_neg]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑(↑normSq (a + b)) = ↑(↑normSq a) + a * star b + b * star a + ↑(↑normSq b)
[PROOFSTEP]
simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r✝ x y z : R
a b c : ℍ[R]
r : R
q : ℍ[R]
⊢ ↑normSq (r • q) = r ^ 2 * ↑normSq q
[PROOFSTEP]
simp only [normSq_def', smul_re, smul_imI, smul_imJ, smul_imK, mul_pow, mul_add, smul_eq_mul]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq (a + b) = ↑normSq a + (a * star b).re + ((b * star a).re + ↑normSq b)
[PROOFSTEP]
simp_rw [normSq_def, star_add, add_mul, mul_add, add_re]
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq a + (a * star b).re + ((b * star a).re + ↑normSq b) =
    ↑normSq a + ↑normSq b + ((a * star b).re + (b * star a).re)
[PROOFSTEP]
abel
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq a + (a * star b).re + ((b * star a).re + ↑normSq b) =
    ↑normSq a + ↑normSq b + ((a * star b).re + (b * star a).re)
[PROOFSTEP]
abel
[GOAL]
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq a + ↑normSq b + ((a * star b).re + (b * star a).re) = ↑normSq a + ↑normSq b + 2 * (a * star b).re
[PROOFSTEP]
rw [← add_re, ← star_mul_star a b, self_add_star', coe_re]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ ↑normSq a = 0 ↔ a = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ normSq.map_zero⟩
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : ↑normSq a = 0
⊢ a = 0
[PROOFSTEP]
rw [normSq_def', add_eq_zero_iff', add_eq_zero_iff', add_eq_zero_iff'] at h
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
[PROOFSTEP]
exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2)
[GOAL]
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
[PROOFSTEP]
all_goals apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ ↑normSq a
[PROOFSTEP]
rw [normSq_def']
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
[PROOFSTEP]
apply_rules [sq_nonneg, add_nonneg]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a✝ a b : ℍ[R]
hab : a * b = 0
⊢ ↑normSq a * ↑normSq b = 0
[PROOFSTEP]
rwa [← map_mul, normSq_eq_zero]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(↑normSq a) ↔ a = ↑a.re
[PROOFSTEP]
rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a
[PROOFSTEP]
exact or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(↑normSq a) ↔ a.re = 0
[PROOFSTEP]
simp_rw [← star_eq_neg]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
[PROOFSTEP]
obtain rfl | hq0 := eq_or_ne a 0
[GOAL]
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 ^ 2 = -↑(↑normSq 0) ↔ star 0 = -0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
[PROOFSTEP]
rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝ : Nontrivial ℍ[R] := instNontrivial
⊢ MonoidWithZero ℍ[R]
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : Nontrivial ℍ[R] := instNontrivial
src✝ : MonoidWithZero ℍ[R] := inferInstance
⊢ 0⁻¹ = 0
[PROOFSTEP]
rw [instInv_inv, star_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a✝ b : ℍ[R]
src✝¹ : Nontrivial ℍ[R] := instNontrivial
src✝ : MonoidWithZero ℍ[R] := inferInstance
a : ℍ[R]
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
letI : Semiring ℍ[R] := inferInstanceAs (Semiring ℍ[R,-1,-1])
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a✝ b : ℍ[R]
src✝¹ : Nontrivial ℍ[R] := instNontrivial
src✝ : MonoidWithZero ℍ[R] := inferInstance
a : ℍ[R]
ha : a ≠ 0
this : Semiring ℍ[R] := inferInstanceAs (Semiring ℍ[R,-1,-1])
⊢ a * a⁻¹ = 1
[PROOFSTEP]
rw [instInv_inv, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
  inv_mul_cancel (normSq_ne_zero.2 ha), coe_one]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
n : ℤ
d : ℕ
hd : d ≠ 0
h : Nat.coprime (Int.natAbs n) d
⊢ ↑(Rat.mk' n d) = ↑n * (↑d)⁻¹
[PROOFSTEP]
rw [← coe_rat_cast, Rat.cast_mk', coe_mul, coe_int_cast, coe_inv, coe_nat_cast]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ (fun x x_1 => x • x_1) q x = ↑q * x
[PROOFSTEP]
rw [← coe_rat_cast, coe_mul_eq_smul]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ (fun x x_1 => x • x_1) q x = ↑q • x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ ((fun x x_1 => x • x_1) q x).re = (↑q • x).re
[PROOFSTEP]
exact DivisionRing.qsmul_eq_mul' _ _
[GOAL]
case a
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ ((fun x x_1 => x • x_1) q x).imI = (↑q • x).imI
[PROOFSTEP]
exact DivisionRing.qsmul_eq_mul' _ _
[GOAL]
case a
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ ((fun x x_1 => x • x_1) q x).imJ = (↑q • x).imJ
[PROOFSTEP]
exact DivisionRing.qsmul_eq_mul' _ _
[GOAL]
case a
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
src✝¹ : GroupWithZero ℍ[R] := instGroupWithZero
src✝ : Ring ℍ[R] := instRing
q : ℚ
x : ℍ[R]
⊢ ((fun x x_1 => x • x_1) q x).imK = (↑q • x).imK
[PROOFSTEP]
exact DivisionRing.qsmul_eq_mul' _ _
[GOAL]
R : Type u_1
inst✝ : LinearOrderedField R
a b : ℍ[R]
q : ℚ
⊢ ↑(↑normSq ↑q) = ↑q ^ 2
[PROOFSTEP]
rw [← coe_rat_cast, normSq_coe, coe_pow]
[GOAL]
R : Type u_1
c₁ c₂ : R
inst✝ : Infinite R
⊢ 1 ≤ 4
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
c₁ c₂ : R
⊢ #ℍ[R,c₁,c₂] = #R ^ 4
[PROOFSTEP]
rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂)]
[GOAL]
R : Type u_1
c₁ c₂ : R
⊢ #(R × R × R × R) = #R ^ 4
[PROOFSTEP]
simp only [mk_prod, lift_id]
[GOAL]
R : Type u_1
c₁ c₂ : R
⊢ #R * (#R * (#R * #R)) = #R ^ 4
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
c₁ c₂ : R
inst✝ : Infinite R
⊢ #ℍ[R,c₁,c₂] = #R
[PROOFSTEP]
rw [mk_quaternionAlgebra, pow_four]
[GOAL]
R : Type u_1
c₁ c₂ : R
⊢ #↑Set.univ = #R ^ 4
[PROOFSTEP]
rw [mk_univ, mk_quaternionAlgebra]
[GOAL]
R : Type u_1
c₁ c₂ : R
inst✝ : Infinite R
⊢ #↑Set.univ = #R
[PROOFSTEP]
rw [mk_univ_quaternionAlgebra, pow_four]


[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝² : OrderedCommMonoid α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : OrderedCommMonoid β
x y : Lex (α × β)
hxy✝ : x ≤ y
z : Lex (α × β)
hxy : x.fst = y.fst ∧ x.snd ≤ y.snd
⊢ (z.fst * x.fst, z.snd * x.snd).fst = (z.fst * y.fst, z.snd * y.snd).fst
[PROOFSTEP]
rw [hxy.1]


[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : NoMaxOrder α
a : α
⊢ NoMaxOrder ↑(Ici a)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) = ↑⊥
[PROOFSTEP]
rw [bot_eq]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
cases' h.lt_or_eq with h2 h2
[GOAL]
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
h2 : sSup ∅ < a
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
simp [h2.not_le]
[GOAL]
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
h2 : sSup ∅ = a
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
simp [h2]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
x✝ : ℕ
⊢ { val := ↑x✝ + 1, property := (_ : (fun x => 0 ≤ x) (↑x✝ + 1)) } = { val := ↑x✝, property := (_ : 0 ≤ ↑x✝) } + 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
⊢ MonoidWithZero { x // 0 ≤ x }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : OrderedCommSemiring α
⊢ CommMonoidWithZero { x // 0 ≤ x }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝¹ : OrderedCommRing α
inst✝ : NoZeroDivisors α
src✝¹ : CanonicallyOrderedAddMonoid { x // 0 ≤ x } := canonicallyOrderedAddMonoid
src✝ : OrderedCommSemiring { x // 0 ≤ x } := orderedCommSemiring
⊢ ∀ {a b : { x // 0 ≤ x }}, a * b = 0 → a = 0 ∨ b = 0
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝¹ : OrderedCommRing α
inst✝ : NoZeroDivisors α
src✝¹ : CanonicallyOrderedAddMonoid { x // 0 ≤ x } := canonicallyOrderedAddMonoid
src✝ : OrderedCommSemiring { x // 0 ≤ x } := orderedCommSemiring
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
⊢ { val := a, property := ha } * { val := b, property := hb } = 0 →
    { val := a, property := ha } = 0 ∨ { val := b, property := hb } = 0
[PROOFSTEP]
simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 ≤ a
⊢ toNonneg a = { val := a, property := h }
[PROOFSTEP]
simp [toNonneg, h]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b
[PROOFSTEP]
cases' b with b hb
[GOAL]
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ { val := b, property := hb } ↔ a ≤ ↑{ val := b, property := hb }
[PROOFSTEP]
simp [toNonneg, hb]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b
[PROOFSTEP]
cases' a with a ha
[GOAL]
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ { val := a, property := ha } < toNonneg b ↔ ↑{ val := a, property := ha } < b
[PROOFSTEP]
simp [toNonneg, ha.not_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ ∀ (a b c : { x // 0 ≤ x }), a - b ≤ c ↔ a ≤ c + b
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
[GOAL]
case mk.mk.mk
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
c : α
hc : 0 ≤ c
⊢ { val := a, property := ha } - { val := b, property := hb } ≤ { val := c, property := hc } ↔
    { val := a, property := ha } ≤ { val := c, property := hc } + { val := b, property := hb }
[PROOFSTEP]
simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le, Subtype.coe_mk]


[GOAL]
α : Type u
inst✝³ : OrderedCancelCommMonoid α
β : Type u_1
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝ : OrderedCommMonoid β := orderedCommMonoid f hf one mul npow
a b c : β
bc : f (a * b) ≤ f (a * c)
⊢ f a * f b ≤ f a * f c
[PROOFSTEP]
rwa [← mul, ← mul]


[GOAL]
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a b : α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le
[GOAL]
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
[PROOFSTEP]
exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩
[GOAL]
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x
[PROOFSTEP]
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
[GOAL]
case intro
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
[PROOFSTEP]
exact h _ ((lt_mul_iff_one_lt_right' b).1 hxb)
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ b * a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ a * b
[PROOFSTEP]
exact le_self_mul
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ (∃ c, b = a * c) → a ≤ b
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a c✝ d c : α
⊢ a ≤ a * c
[PROOFSTEP]
exact le_self_mul
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ b ↔ ∃ c, b = c * a
[PROOFSTEP]
simp only [mul_comm _ a, le_iff_exists_mul]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b
[PROOFSTEP]
simp only [one_lt_iff_ne_one, Ne.def, mul_eq_one_iff, not_and_or]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
⊢ ∃ c x, a * c = b
[PROOFSTEP]
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b
[PROOFSTEP]
refine' ⟨c, one_lt_iff_ne_one.2 _, hc.symm⟩
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1
[PROOFSTEP]
rintro rfl
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
hc : b = a * 1
⊢ False
[PROOFSTEP]
simp [hc, lt_irrefl] at h
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a ≤ c
⊢ a = 1 * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a ≤ b
⊢ a = a * 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c
[PROOFSTEP]
rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
[GOAL]
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
[PROOFSTEP]
intro c
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
[PROOFSTEP]
rw [and_comm, and_congr_left_iff, gt_iff_lt]
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)
[PROOFSTEP]
rintro rfl
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c ↔ 1 < c
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → 1 < c
[PROOFSTEP]
rw [one_lt_iff_ne_one]
[GOAL]
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → c ≠ 1
[PROOFSTEP]
apply mt
[GOAL]
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ c = 1 → a = a * c
[PROOFSTEP]
rintro rfl
[GOAL]
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a ≠ a * c
[PROOFSTEP]
rw [← (self_le_mul_right a c).lt_iff_ne]
[GOAL]
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a < a * c
[PROOFSTEP]
apply lt_mul_of_one_lt_right'
[GOAL]
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
cases' le_total a b with hb hb
[GOAL]
case inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hb, le_mul_right]
[GOAL]
case inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
cases' le_total a c with hc hc
[GOAL]
case inr.inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hc, le_mul_left]
[GOAL]
case inr.inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hb, hc]
[GOAL]
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
⊢ min (a * b) c = min (min a c * min b c) c
[PROOFSTEP]
simpa [min_comm _ c] using min_mul_distrib c a b