awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ x_1.re * x_3.re + x_2.re * x_3.re + (a * x_1.im * x_3.im + a * x_2.im * x_3.im) =
    x_1.re * x_3.re + a * x_1.im * x_3.im + (x_2.re * x_3.re + a * x_2.im * x_3.im)

Tactic:
abel
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ x_1.re * x_3.im + x_2.re * x_3.im + (x_1.im * x_3.re + x_2.im * x_3.re) +
      (b * x_1.im * x_3.im + b * x_2.im * x_3.im) =
    x_1.re * x_3.im + x_1.im * x_3.re + b * x_1.im * x_3.im + (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)

Tactic:
abel
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
re : (0 * x_1).re = QuadraticAlgebra.re (a := a) (b := b) 0
im : (0 * x_1).im = QuadraticAlgebra.im (a := a) (b := b) 0
⊢ 0 * x_1 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (0 * x_1).re = re (a := a) (b := b) 0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (0 * x_1).im = im (a := a) (b := b) 0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
re : (x_1 * 0).re = QuadraticAlgebra.re (a := a) (b := b) 0
im : (x_1 * 0).im = QuadraticAlgebra.im (a := a) (b := b) 0
⊢ x_1 * 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (x_1 * 0).re = re (a := a) (b := b) 0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (x_1 * 0).im = im (a := a) (b := b) 0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
re : (QuadraticAlgebra.C r * x).re = (r • x).re
im : (QuadraticAlgebra.C r * x).im = (r • x).im
⊢ QuadraticAlgebra.C r * x = r • x

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
x y : R
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).im
⊢ QuadraticAlgebra.C (x * y) = HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ re (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ im (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
re : (1 * x_1).re = x_1.re
im : (1 * x_1).im = x_1.im
⊢ 1 * x_1 = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (1 * x_1).re = x_1.re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (1 * x_1).im = x_1.im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
re : (x_1 * 1).re = x_1.re
im : (x_1 * 1).im = x_1.im
⊢ x_1 * 1 = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (x_1 * 1).re = x_1.re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : QuadraticAlgebra R a b
⊢ (x_1 * 1).im = x_1.im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonAssocSemiring R
n : ℕ
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
im :
  (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).im =
    QuadraticAlgebra.im (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b } =
    { re := (↑n : R) * x, im := (↑n : R) * y }

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonAssocSemiring R
n : ℕ
x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NonAssocSemiring R
n : ℕ
x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).im =
    im (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Semiring R
z : QuadraticAlgebra R a b
⊢ (linearEquivTuple a b : (a : QuadraticAlgebra R a b) → Fin 2 → R) z = ![z.re, z.im]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Semiring R
x : Fin 2 → R
⊢ Eq (α := QuadraticAlgebra R a b)
    ((LinearEquiv.symm (linearEquivTuple a b) : (a_1 : Fin 2 → R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
    ({ re := x 0, im := x 1 } : QuadraticAlgebra R a b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Semiring R
x : QuadraticAlgebra R a b
⊢ (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) x : Fin 2 →₀ R) : (a : Fin 2) → R) =
    ![x.re, x.im]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : Semiring R
⊢ Module.Finite R (QuadraticAlgebra R a b)

Tactic:
.of_basis (basis a b)

Premises used: QuadraticAlgebra.basis, Module.Finite.of_basis
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : Semiring R
⊢ Module.Free R (QuadraticAlgebra R a b)

Tactic:
.of_basis (basis a b)

Premises used: Module.Free.of_basis, QuadraticAlgebra.basis
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Semiring R
inst_1 : StrongRankCondition R
⊢ Module.rank R (QuadraticAlgebra R a b) = 2

Tactic:
simp [rank_eq_card_basis (basis a b)]

Premises used: rank_eq_card_basis, QuadraticAlgebra.basis
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Semiring R
inst_1 : StrongRankCondition R
⊢ Module.finrank R (QuadraticAlgebra R a b) = 2

Tactic:
simp [Module.finrank, rank_eq_two]

Premises used: QuadraticAlgebra.rank_eq_two, Module.finrank
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
re : (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re
im : (x_1 * x_2 * x_3).im = (x_1 * (x_2 * x_3)).im
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
re :
  (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.re +
      a * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
    x_1.re * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
      a * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)
⊢ (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
im :
  (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.im +
        (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.re +
      b * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
    x_1.re * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im) +
        x_1.im * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
      b * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)
⊢ (x_1 * x_2 * x_3).im = (x_1 * (x_2 * x_3)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.re +
      a * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
    x_1.re * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
      a * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.im +
        (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.re +
      b * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
    x_1.re * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im) +
        x_1.im * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
      b * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 : QuadraticAlgebra R a b
re : (x_1 * x_2).re = (x_2 * x_1).re
im : (x_1 * x_2).im = (x_2 * x_1).im
⊢ x_1 * x_2 = x_2 * x_1

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 : QuadraticAlgebra R a b
re : x_1.re * x_2.re + a * x_1.im * x_2.im = x_2.re * x_1.re + a * x_2.im * x_1.im
⊢ (x_1 * x_2).re = (x_2 * x_1).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 : QuadraticAlgebra R a b
im : x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im = x_2.re * x_1.im + x_2.im * x_1.re + b * x_2.im * x_1.im
⊢ (x_1 * x_2).im = (x_2 * x_1).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 : QuadraticAlgebra R a b
⊢ x_1.re * x_2.re + a * x_1.im * x_2.im = x_2.re * x_1.re + a * x_2.im * x_1.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 x_2 : QuadraticAlgebra R a b
⊢ x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im = x_2.re * x_1.im + x_2.im * x_1.re + b * x_2.im * x_1.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
re :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
    (QuadraticAlgebra.re (a := a) (b := b) 1 : R)
im :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
    (QuadraticAlgebra.im (a := a) (b := b) 1 : R)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1) : QuadraticAlgebra R a b) (1 : QuadraticAlgebra R a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
    (re (a := a) (b := b) 1 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
    (im (a := a) (b := b) 1 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y)) =
    HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
re :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
    (QuadraticAlgebra.re (a := a) (b := b) 0 : R)
im :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
    (QuadraticAlgebra.im (a := a) (b := b) 0 : R)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0) : QuadraticAlgebra R a b) (0 : QuadraticAlgebra R a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
    (re (a := a) (b := b) 0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
    (im (a := a) (b := b) 0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y)) =
    HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
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_1 : CommSemiring S
inst_2 : Algebra S R
s : S
z : QuadraticAlgebra R a b
re :
  (HMul.hMul (α := QuadraticAlgebra R a b)
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)
        z).re =
    (HMul.hMul (β := QuadraticAlgebra R a b) z
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)).re
im :
  (HMul.hMul (α := QuadraticAlgebra R a b)
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)
        z).im =
    (HMul.hMul (β := QuadraticAlgebra R a b) z
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)).im
⊢ HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      z =
    HMul.hMul (β := QuadraticAlgebra R a b) z
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)

Tactic:
ext