[GOAL]
x x✝ : PEmpty
⊢ PEmpty
[PROOFSTEP]
cases x
[GOAL]
x y z : PEmpty
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
cases x


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₁ q₂ : Basis A c₁ c₂
hi : q₁.i = q₂.i
hj : q₁.j = q₂.j
⊢ q₁ = q₂
[PROOFSTEP]
cases q₁
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₂ : Basis A c₁ c₂
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i =
    q₂.i
hj :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j =
    q₂.j
⊢ { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ } = q₂
[PROOFSTEP]
rename_i q₁_i_mul_j _
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₂ : Basis A c₁ c₂
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₁_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝ }.i =
    q₂.i
hj :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝ }.j =
    q₂.j
⊢ { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j, j_mul_i := j_mul_i✝ } =
    q₂
[PROOFSTEP]
cases q₂
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }
[PROOFSTEP]
rename_i q₂_i_mul_j _
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j, j_mul_i := j_mul_i✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_k
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ k✝¹ = k✝
[PROOFSTEP]
rw [← q₁_i_mul_j, ← q₂_i_mul_j]
[GOAL]
case mk.mk.e_k
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ i✝¹ * j✝¹ = i✝ * j✝
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } = c₁ • 1
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re = (c₁ • 1).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI = (c₁ • 1).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ = (c₁ • 1).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK = (c₁ • 1).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } = c₂ • 1
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re = (c₂ • 1).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI = (c₂ • 1).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ = (c₂ • 1).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK = (c₂ • 1).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    -{ re := 0, imI := 0, imJ := 0, imK := 1 }
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.i * q.k = c₁ • q.j
[PROOFSTEP]
rw [← i_mul_j, ← mul_assoc, i_mul_i, smul_mul_assoc, one_mul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.i = -c₁ • q.j
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, j_mul_i, mul_neg, i_mul_k, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.j = c₂ • q.i
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.j * q.k = -c₂ • q.i
[PROOFSTEP]
rw [← i_mul_j, ← mul_assoc, j_mul_i, neg_mul, k_mul_j, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.k = -((c₁ * c₂) • 1)
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_neg, ← mul_assoc, i_mul_i,
  smul_mul_assoc, one_mul, neg_mul, smul_mul_assoc, j_mul_j, smul_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ lift q 0 = 0
[PROOFSTEP]
simp [lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ lift q 1 = 1
[PROOFSTEP]
simp [lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ lift q (x + y) = lift q x + lift q y
[PROOFSTEP]
simp [lift, add_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ lift q (x * y) = lift q x * lift q y
[PROOFSTEP]
simp only [lift, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re • 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) +
            (x.imI * y.imK) • (q.i * q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) +
          (x.imJ * y.imK) • (q.j * q.k)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) +
        (x.imK * y.imK) • (q.k * q.k))
[PROOFSTEP]
simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • c₁ • 1 + (x.imI * y.imJ) • q.k + (x.imI * y.imK) • c₁ • q.j) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • -q.k + (x.imJ * y.imJ) • c₂ • 1 + (x.imJ * y.imK) • -c₂ • q.i) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₂ • q.i +
        (x.imK * y.imK) • -((c₁ * c₂) • 1))
[PROOFSTEP]
simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ← add_assoc, mul_neg, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI * c₁) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK * c₁) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((x.imK * y.imK * (c₁ * c₂)) • 1)
[PROOFSTEP]
simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI * c₁) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK * c₁) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((c₁ * c₂ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [mul_comm _ c₁, mul_right_comm _ _ c₁]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * (x.imI * y.imI)) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * (x.imI * y.imK)) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((c₁ * c₂ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [mul_comm _ c₂, mul_right_comm _ _ c₂]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * (x.imI * y.imI)) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * (x.imI * y.imK)) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * (x.imJ * y.imJ)) • 1 +
              -((c₂ * (x.imJ * y.imK)) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (c₂ * (x.imK * y.imJ)) • q.i +
      -((c₂ * c₁ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [← mul_comm c₁ c₂, ← mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
simp [sub_eq_add_neg, add_smul, ← add_assoc]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₂ * x.imJ * y.imJ) • 1 + -((c₁ * c₂ * x.imK * y.imK) • 1) +
                            (x.re * y.imI) • q.i +
                          (x.imI * y.re) • q.i +
                        -((c₂ * x.imJ * y.imK) • q.i) +
                      (c₂ * x.imK * y.imJ) • q.i +
                    (x.re * y.imJ) • q.j +
                  (c₁ * x.imI * y.imK) • q.j +
                (x.imJ * y.re) • q.j +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.re * y.imK) • q.k +
          (x.imI * y.imJ) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₂ * x.imJ * y.imJ) • 1 + -((c₁ * c₂ * x.imK * y.imK) • 1) +
                            (x.re * y.imI) • q.i +
                          (x.imI * y.re) • q.i +
                        -((c₂ * x.imJ * y.imK) • q.i) +
                      (c₂ * x.imK * y.imJ) • q.i +
                    (x.re * y.imJ) • q.j +
                  (c₁ * x.imI * y.imK) • q.j +
                (x.imJ * y.re) • q.j +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.re * y.imK) • q.k +
          (x.imI * y.imJ) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
r : R
x : ℍ[R,c₁,c₂]
⊢ lift q (r • x) = r • lift q x
[PROOFSTEP]
simp [lift, mul_smul, ← Algebra.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.i * ↑F q.i = c₁ • 1
[PROOFSTEP]
rw [← F.map_mul, q.i_mul_i, F.map_smul, F.map_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.j * ↑F q.j = c₂ • 1
[PROOFSTEP]
rw [← F.map_mul, q.j_mul_j, F.map_smul, F.map_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.i * ↑F q.j = ↑F q.k
[PROOFSTEP]
rw [← F.map_mul, q.i_mul_j]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.j * ↑F q.i = -↑F q.k
[PROOFSTEP]
rw [← F.map_mul, q.j_mul_i, F.map_neg]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ Basis.compHom (Basis.self R) (Basis.liftHom q) = q
[PROOFSTEP]
ext
[GOAL]
case hi
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ (Basis.compHom (Basis.self R) (Basis.liftHom q)).i = q.i
[PROOFSTEP]
simp [Basis.lift]
[GOAL]
case hj
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ (Basis.compHom (Basis.self R) (Basis.liftHom q)).j = q.j
[PROOFSTEP]
simp [Basis.lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
⊢ Basis.liftHom (Basis.compHom (Basis.self R) F) = F
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑(Basis.liftHom (Basis.compHom (Basis.self R) F)) x✝ = ↑F x✝
[PROOFSTEP]
dsimp [Basis.lift]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x✝.re + x✝.imI • ↑F { re := 0, imI := 1, imJ := 0, imK := 0 } +
        x✝.imJ • ↑F { re := 0, imI := 0, imJ := 1, imK := 0 } +
      x✝.imK • ↑F { re := 0, imI := 0, imJ := 0, imK := 1 } =
    ↑F x✝
[PROOFSTEP]
rw [← F.commutes]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑F (↑(algebraMap R ℍ[R,c₁,c₂]) x✝.re) + x✝.imI • ↑F { re := 0, imI := 1, imJ := 0, imK := 0 } +
        x✝.imJ • ↑F { re := 0, imI := 0, imJ := 1, imK := 0 } +
      x✝.imK • ↑F { re := 0, imI := 0, imJ := 0, imK := 1 } =
    ↑F x✝
[PROOFSTEP]
simp only [← F.commutes, ← F.map_smul, ← F.map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑F
      { re := x✝.re + 0 + 0 + 0, imI := 0 + x✝.imI • 1 + 0 + 0, imJ := 0 + 0 + x✝.imJ • 1 + 0,
        imK := 0 + 0 + 0 + x✝.imK • 1 } =
    ↑F x✝
[PROOFSTEP]
congr
[GOAL]
case H.h.e_6.h.e_re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ x✝.re + 0 + 0 + 0 = x✝.re
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + x✝.imI • 1 + 0 + 0 = x✝.imI
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + 0 + x✝.imJ • 1 + 0 = x✝.imJ
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + 0 + 0 + x✝.imK • 1 = x✝.imK
[PROOFSTEP]
simp


[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : Stream'.Seq.get? g.s n = some gp
nth_conts_aux_eq : continuantsAux g n = ppred
succ_nth_conts_aux_eq : continuantsAux g (n + 1) = pred
⊢ continuantsAux g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
simp [*, continuantsAux, nextContinuants, nextDenominator, nextNumerator]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : Stream'.Seq.get? g.s n = some gp
nth_conts_aux_eq : continuantsAux g n = ppred
succ_nth_conts_aux_eq : continuantsAux g (n + 1) = pred
⊢ continuants g (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
simp [nth_cont_eq_succ_nth_cont_aux, continuantsAux_recurrence nth_s_eq nth_conts_aux_eq succ_nth_conts_aux_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_conts_eq : continuants g n = ppred
succ_nth_conts_eq : continuants g (n + 1) = pred
⊢ continuants g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
rw [nth_cont_eq_succ_nth_cont_aux] at nth_conts_eq succ_nth_conts_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_conts_eq : continuantsAux g (n + 1) = ppred
succ_nth_conts_eq : continuantsAux g (n + 1 + 1) = pred
⊢ continuants g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
exact continuants_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_num_eq : numerators g n = ppredA
succ_nth_num_eq : numerators g (n + 1) = predA
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredA
[PROOFSTEP]
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.a = ppredA
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_num_eq : numerators g n = ppredA
succ_nth_num_eq : numerators g (n + 1) = predA
⊢ ∃ conts, continuants g n = conts ∧ conts.a = ppredA
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredConts.a
[PROOFSTEP]
exact exists_conts_a_of_num nth_num_eq
[GOAL]
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredConts.a
[PROOFSTEP]
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants (n + 1) = conts ∧ conts.a = predA
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ ∃ conts, continuants g (n + 1) = conts ∧ conts.a = predA
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_num_eq : numerators g (n + 1) = predConts.a
⊢ numerators g (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
[PROOFSTEP]
exact exists_conts_a_of_num succ_nth_num_eq
[GOAL]
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_num_eq : numerators g (n + 1) = predConts.a
⊢ numerators g (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
[PROOFSTEP]
rw [num_eq_conts_a, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_denom_eq : denominators g n = ppredB
succ_nth_denom_eq : denominators g (n + 1) = predB
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredB
[PROOFSTEP]
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.b = ppredB
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_denom_eq : denominators g n = ppredB
succ_nth_denom_eq : denominators g (n + 1) = predB
⊢ ∃ conts, continuants g n = conts ∧ conts.b = ppredB
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredConts.b
[PROOFSTEP]
exact exists_conts_b_of_denom nth_denom_eq
[GOAL]
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredConts.b
[PROOFSTEP]
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants (n + 1) = conts ∧ conts.b = predB
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ ∃ conts, continuants g (n + 1) = conts ∧ conts.b = predB
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_denom_eq : denominators g (n + 1) = predConts.b
⊢ denominators g (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
[PROOFSTEP]
exact exists_conts_b_of_denom succ_nth_denom_eq
[GOAL]
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_denom_eq : denominators g (n + 1) = predConts.b
⊢ denominators g (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
[PROOFSTEP]
rw [denom_eq_conts_b, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]


[GOAL]
R : Type u_1
inst✝ : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c
[PROOFSTEP]
simp [discrim]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * x * x + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2
[PROOFSTEP]
rw [discrim]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * x * x + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
[PROOFSTEP]
linear_combination -4 * a * h
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
⊢ a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
[PROOFSTEP]
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
rw [discrim] at h
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
apply mul_left_cancel₀ ha
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ 2 * 2 * a * (a * x * x + b * x + c) = 2 * 2 * a * 0
[PROOFSTEP]
linear_combination -h
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
[PROOFSTEP]
rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
[PROOFSTEP]
field_simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b + s ∨ x * (2 * a) = -b - s
[PROOFSTEP]
apply or_congr
[GOAL]
case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ↔ x * (2 * a) = -b + s
[PROOFSTEP]
constructor
[GOAL]
case h₁.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b → x * (2 * a) = -b + s
[PROOFSTEP]
intro h'
[GOAL]
case h₁.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ x * (2 * a) = -b + s → s = 2 * a * x + b
[PROOFSTEP]
intro h'
[GOAL]
case h₁.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : s = 2 * a * x + b
⊢ x * (2 * a) = -b + s
[PROOFSTEP]
linear_combination -h'
[GOAL]
case h₁.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : x * (2 * a) = -b + s
⊢ s = 2 * a * x + b
[PROOFSTEP]
linear_combination -h'
[GOAL]
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b - s
[PROOFSTEP]
constructor
[GOAL]
case h₂.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) → x * (2 * a) = -b - s
[PROOFSTEP]
intro h'
[GOAL]
case h₂.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ x * (2 * a) = -b - s → s = -b + -(2 * a * x)
[PROOFSTEP]
intro h'
[GOAL]
case h₂.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : s = -b + -(2 * a * x)
⊢ x * (2 * a) = -b - s
[PROOFSTEP]
linear_combination h'
[GOAL]
case h₂.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : x * (2 * a) = -b - s
⊢ s = -b + -(2 * a * x)
[PROOFSTEP]
linear_combination h'
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
h : ∃ s, discrim a b c = s * s
⊢ ∃ x, a * x * x + b * x + c = 0
[PROOFSTEP]
rcases h with ⟨s, hs⟩
[GOAL]
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ ∃ x, a * x * x + b * x + c = 0
[PROOFSTEP]
use(-b + s) / (2 * a)
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a)) * ((-b + s) / (2 * a)) + b * ((-b + s) / (2 * a)) + c = 0
[PROOFSTEP]
rw [quadratic_eq_zero_iff ha hs]
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
[PROOFSTEP]
have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ discrim a b c = 0 * 0
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
[PROOFSTEP]
rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ discrim a b c ≤ 0
[PROOFSTEP]
rw [discrim, sq]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a :=
  lt_trichotomy a
    0
      -- if a < 0
[GOAL]
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
  tendsto_atBot_add_const_right _ c
    ((tendsto_atBot_add_const_right _ b (tendsto_id.neg_const_mul_atTop ha)).atBot_mul_atTop tendsto_id)
[GOAL]
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
rcases(this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
[GOAL]
case inl.intro
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
exact
  False.elim
    ((h x).not_lt <| by rwa [← add_mul])
      -- if a = 0
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * x * x + b * x + c < 0
[PROOFSTEP]
rwa [← add_mul]
[GOAL]
case inr.inl
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl.inl
K : Type u_1
inst✝ : LinearOrderedField K
c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0
[PROOFSTEP]
have := h ((-c - 1) / b)
[GOAL]
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + b * ((-c - 1) / b) + c
⊢ b * b - 4 * 0 * c ≤ 0
[PROOFSTEP]
rw [mul_div_cancel' _ hb] at this
[GOAL]
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0
[PROOFSTEP]
linarith
  -- if a > 0
[GOAL]
case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
[GOAL]
case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c ≤ 0
[PROOFSTEP]
convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
[GOAL]
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c))
[PROOFSTEP]
field_simp [ha.ne']
[GOAL]
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ (b * b - 4 * a * c) * (2 * a * (2 * a) * (2 * a)) =
    -(4 * a * (a * b * b * (2 * a) + -(b * b * (2 * a * (2 * a))) + c * (2 * a * (2 * a) * (2 * a))))
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), a * x * x + b * x + c ≤ 0
⊢ ∀ (x : K), 0 ≤ -a * x * x + -b * x + -c
[PROOFSTEP]
simpa only [neg_mul, ← neg_add, neg_nonneg]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
⊢ discrim a b c < 0
[PROOFSTEP]
have : ∀ x : K, 0 ≤ a * x * x + b * x + c := fun x => le_of_lt (h x)
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ discrim a b c < 0
[PROOFSTEP]
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
⊢ False
[PROOFSTEP]
have := h (-b / (2 * a))
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
⊢ False
[PROOFSTEP]
have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
  rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
[PROOFSTEP]
rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝¹ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this✝ : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), a * x * x + b * x + c < 0
⊢ ∀ (x : K), 0 < -a * x * x + -b * x + -c
[PROOFSTEP]
simpa only [neg_mul, ← neg_add, neg_pos]