mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.re + a * x✝¹.im * x✝.im = x✝.re * x✝¹.re + a * x✝.im * x✝¹.im

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im = x✝.re * x✝¹.im + x✝.im * x✝¹.re + b * x✝.im * x✝¹.im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.re + a * x✝¹.im * x✝.im = x✝.re * x✝¹.re + a * x✝.im * x✝¹.im

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im = x✝.re * x✝¹.im + x✝.im * x✝¹.re + b * x✝.im * x✝¹.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ a.re * b.re + a✝ * a.im * b.im + b✝ * (a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    (b.re + b✝ * b.im) * (a.re + b✝ * a.im) + a✝ * b.im * a.im

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ -(a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    -((b.re + b✝ * b.im) * a.im) + -(b.im * (a.re + b✝ * a.im)) + b✝ * b.im * a.im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ a.re * b.re + a✝ * a.im * b.im + b✝ * (a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    (b.re + b✝ * b.im) * (a.re + b✝ * a.im) + a✝ * b.im * a.im

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ -(a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    -((b.re + b✝ * b.im) * a.im) + -(b.im * (a.re + b✝ * a.im)) + b✝ * b.im * a.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).re = re 1

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).im = im 1

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).re = re 1

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).im = im 1
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).re

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).re

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).re = re 0

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).im = im 0

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).re = re 0

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).re = (z.im • (ω - star ω)).re

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).im = (z.im • (ω - star ω)).im

Tactic:
<;>

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).re = (z.im • (ω - star ω)).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).im = (z.im • (ω - star ω)).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).re

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).re

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ b * z.im = z.im * b

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.im + z.im = z.im * (1 + 1)

Tactic:
<;>

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ b * z.im = z.im * b

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.im + z.im = z.im * (1 + 1)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        z).re =
    (z *
        { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s).re

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        z).im =
    (z *
        { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s).im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        z).re =
    (z *
        { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s).re

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        z).im =
    (z *
        { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).re =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).re

pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).im =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).re =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).re

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).im =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).re = (z * star z).re

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).im = (z * star z).im

Tactic:
<;>

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).re = (z * star z).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).im = (z * star z).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

pp: case im
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

case im
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.re * z.re + z.im * (b * z.re) - z.im * (a * z.im) = z.re * (z.re + b * z.im) + -(z.im * (a * z.im))

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))

Tactic:
<;>

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.re * z.re + z.im * (b * z.re) - z.im * (a * z.im) = z.re * (z.re + b * z.im) + -(z.im * (a * z.im))

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ⇑((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) =
    ⇑((basis a b).repr (((Matrix.toLin (basis a b) (basis a b)) !![z.re, a * z.im; z.im, z.re + b * z.im]) w))

Tactic:
Matrix.repr_toLin

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ⇑((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec ⇑((basis a b).repr w)
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k = q' i * ∏ i ∈ s, g i ^ n i + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
← Finset.mul_prod_erase s _ hi,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.im + z.im * w.re + b * z.im * w.im = w.re * z.im + w.im * (z.re + b * z.im)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)

case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.im + z.im * w.re + b * z.im * w.im = w.re * z.im + w.im * (z.re + b * z.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp.re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.re = re 0

pp: case mp.im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.im = im 0

Tactic:
<;>

Goal state after:
case mp.re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.re = re 0

case mp.im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).re = (z + star z).re

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).im = (z + star z).im

Tactic:
<;>

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).re = (z + star z).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).im = (z + star z).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.re = re 0

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.im = im 0

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.re = re 0

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ (↑q).re = (↑q.num / ↑q.den).re

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ (↑q).im = (↑q.num / ↑q.den).im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ (↑q).re = (↑q.num / ↑q.den).re

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im