mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : (∏ x ∈ s, g x) * g i * (q₁ - q₂) = 0
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
(hpm.mul hg.1).mul_right_eq_zero_iff

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
ext

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✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² • (x✝¹ + x✝)).re = (x✝² • x✝¹ + x✝² • 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✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² • (x✝¹ + x✝)).im = (x✝² • x✝¹ + x✝² • x✝).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = { re := a, im := b }

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).re = { re := a, im := b }.re

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = { re := a, im := b }.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = a • 1 + b • ω

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).re = (a • 1 + b • ω).re

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = (a • 1 + b • ω).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ ω * { re := x, im := y } = { re := a * y, im := x + b * y }

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ (ω * { re := x, im := y }).re = { re := a * y, im := x + b * y }.re

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ (ω * { re := x, im := y }).im = { re := a * y, im := x + b * y }.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ (ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y }).re =
    { re := a * n * y, im := n * x + n * b * y }.re

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ (ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y }).im =
    { re := a * n * y, im := n * x + n * b * y }.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x + y • ω

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y }.re = ((algebraMap R (QuadraticAlgebra R a b)) x + y • ω).re

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y }.im = ((algebraMap R (QuadraticAlgebra R a b)) x + y • ω).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r✝ : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ (r + s) • x = r • x + s • x

Tactic:
ext

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✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).re = (r • x + 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✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).im = (r • x + s • x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ 0 • x = 0

Tactic:
ext

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✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ (0 • x).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✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ (0 • x).im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
⊢ QuadraticAlgebra.C ↑0 = 0

Tactic:
ext

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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑0).im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ QuadraticAlgebra.C ↑(n + 1) = QuadraticAlgebra.C ↑n + 1

Tactic:
ext

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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).re = (QuadraticAlgebra.C ↑n + 1).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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).im = (QuadraticAlgebra.C ↑n + 1).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ QuadraticAlgebra.C (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
ext

Goal state after:
case re
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).re = (OfNat.ofNat n).re

case im
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).im = (OfNat.ofNat n).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ QuadraticAlgebra.C ↑↑n = ↑n

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext

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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * 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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * (x✝¹ + x✝)).im = (x✝² * x✝¹ + x✝² * x✝).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext

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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ ((x✝² + x✝¹) * x✝).re = (x✝² * x✝ + x✝¹ * 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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ ((x✝² + x✝¹) * x✝).im = (x✝² * x✝ + x✝¹ * x✝).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 0 * x✝ = 0

Tactic:
ext

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✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (0 * x✝).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✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (0 * x✝).im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 0 = 0

Tactic:
ext

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✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 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✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 0).im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ QuadraticAlgebra.C r * x = r • x

Tactic:
ext

Goal state after:
case re
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ (QuadraticAlgebra.C r * x).re = (r • x).re

case im
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ (QuadraticAlgebra.C r * x).im = (r • x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ QuadraticAlgebra.C (x * y) = QuadraticAlgebra.C x * QuadraticAlgebra.C y

Tactic:
ext

Goal state after:
case re
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (QuadraticAlgebra.C (x * y)).re = (QuadraticAlgebra.C x * QuadraticAlgebra.C y).re

case im
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (QuadraticAlgebra.C (x * y)).im = (QuadraticAlgebra.C x * QuadraticAlgebra.C y).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ (fun u ↦
        { toFun := fun z ↦ z.re • 1 + z.im • ↑u, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ })
      ((fun f ↦ ⟨f ω, ⋯⟩) f) =
    f

Tactic:
ext

Goal state after:
K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ ((fun u ↦
          { toFun := fun z ↦ z.re • 1 + z.im • ↑u, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
            commutes' := ⋯ })
        ((fun f ↦ ⟨f ω, ⋯⟩) f))
      ω =
    f ω
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 1 * x✝ = x✝

Tactic:
ext

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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (1 * x✝).re = 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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (1 * x✝).im = x✝.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 1 = x✝

Tactic:
ext

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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).re = 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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).im = x✝.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ { re := x, im := y } * star { re := x, im := y } =
    (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
        (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
          (algebraMap R (QuadraticAlgebra R a b)) y -
      (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
        (algebraMap R (QuadraticAlgebra R a b)) y

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ ({ re := x, im := y } * star { re := x, im := y }).re =
    ((algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
          (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
            (algebraMap R (QuadraticAlgebra R a b)) y -
        (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
          (algebraMap R (QuadraticAlgebra R a b)) y).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ ({ re := x, im := y } * star { re := x, im := y }).im =
    ((algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
          (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
            (algebraMap R (QuadraticAlgebra R a b)) y -
        (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
          (algebraMap R (QuadraticAlgebra R a b)) y).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
ext

Goal state after:
case re
R : Type u_1
a b : R
inst✝ : NonAssocSemiring 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✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: 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✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext

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✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * 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
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹ * x✝).im = (x✝² * (x✝¹ * x✝)).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ star (a * b) = star b * star a

Tactic:
ext

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✝
⊢ (star (a * b)).re = (star b * star a).re

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

Goal state before:
pp: 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✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext

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✝¹ * x✝).re = (x✝ * 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
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).im = (x✝ * x✝¹).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: 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) = 1

Tactic:
ext

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: 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)) =
    QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
ext

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: 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) = 0

Tactic:
ext

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: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z - star z = z.im • (ω - star ω)

Tactic:
ext

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: 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)) =
    QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
ext

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: 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 =
    z *
      { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s

Tactic:
ext

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