awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

Tactic:
not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')

Premises used: Nat.sub_pos_of_lt, dvd_pow, LT.lt.ne', dvd_refl, not_isUnit_of_not_isUnit_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

Tactic:
exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')

Premises used: Nat.sub_pos_of_lt, dvd_pow, LT.lt.ne', dvd_refl, not_isUnit_of_not_isUnit_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
(pow_mul_pow_sub q h.le).symm

Premises used: LT.lt.le, Eq.symm, pow_mul_pow_sub
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
exact (pow_mul_pow_sub q h.le).symm

Premises used: LT.lt.le, Eq.symm, pow_mul_pow_sub
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
m n : ℕ
⊢ q ^ m = q ^ n ↔ m = n

Tactic:
(pow_injective_of_not_isUnit hq hq').eq_iff

Premises used: pow_injective_of_not_isUnit, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_3
N : Type u_4
F : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
inst_4 : IsLocalHom.{u_3, u_4, u_5} (R := M) (S := N) f
a b : M
hab : IsRelPrime.{u_4} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
⊢ IsRelPrime a b

Tactic:
fun _ h₁ h₂ ↦ .of_map _ _ (hab (map_dvd f h₁) (map_dvd f h₂))

Premises used: IsRelPrime, IsUnit.of_map, map_dvd
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : Zero R
inst_1 : One R
⊢ Eq.{u_2 + 1} (α := R) (re (a := a) (b := b) ω) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : Zero R
inst_1 : One R
⊢ Eq.{u_2 + 1} (α := R) (im (a := a) (b := b) ω) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
re : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re = QuadraticAlgebra.re (a := a) (b := b) { re := a, im := b }
im : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im = QuadraticAlgebra.im (a := a) (b := b) { re := a, im := b }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω = { re := a, im := b }

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re = re (a := a) (b := b) { re := a, im := b }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im = im (a := a) (b := b) { re := a, im := b }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re =
    (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).re
im :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im =
    (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).im
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω =
    HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re =
    (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im =
    (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := a * y, im := x + b * y }
im :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).im =
    QuadraticAlgebra.im (a := a) (b := b) { re := a * y, im := x + b * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * y, im := x + b * y }

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).re =
    re (a := a) (b := b) { re := a * y, im := x + b * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).im =
    im (a := a) (b := b) { re := a * y, im := x + b * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → 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 := a * n * y, im := n * x + n * b * y }
im :
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → 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 := a * n * y, im := n * x + n * b * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
      { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * n * y, im := n * x + n * b * y }

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    re (a := a) (b := b) { re := a * n * y, im := n * x + n * b * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
im : n * x + b * n * y = n * x + n * b * y
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → 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 := a * n * y, im := n * x + n * b * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
⊢ n * x + b * n * y = n * x + n * b * y

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
re :
  QuadraticAlgebra.re (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
    (HAdd.hAdd (α := QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
        (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
    (HAdd.hAdd (α := QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
        (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).im
⊢ { re := x, im := y } =
    HAdd.hAdd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
      (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ re (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
    (HAdd.hAdd (α := QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
        (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ im (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
    (HAdd.hAdd (α := QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
        (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
f g : QuadraticAlgebra R a b →ₐ[R] A
h : Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) ω : A) ((g : (a : QuadraticAlgebra R a b) → A) ω : A)
H :
  ∀ (x y : R),
    Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)
      ((g : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)
⊢ f = g

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
f g : QuadraticAlgebra R a b →ₐ[R] A
h : Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) ω : A) ((g : (a : QuadraticAlgebra R a b) → A) ω : A)
x y : R
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)
    ((g : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)

Tactic:
simp [mk_eq_add_smul_omega, h]

Premises used: QuadraticAlgebra.mk_eq_add_smul_omega
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := A) (re (a := a) (b := b) 1) 1 +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (im (a := a) (b := b) 1) (↑u : A) =
    1

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
symm :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
⊢ HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A) =
    (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A))

Tactic:
symm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
simp :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.im * w.re) • (↑u : A) + (z.re * w.im) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))

Tactic:
simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]

Premises used: add_mul, add_assoc, smul_mul_smul, mul_add, mul_one, one_mul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.im * w.re) • (↑u : A) + (z.re * w.im) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))

Tactic:
apply add_add_add_comm'

Premises used: add_add_add_comm'
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))

Tactic:
congr 1
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + ((z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)

Tactic:
simp only [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a e_a₁ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + ((z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)

Tactic:
rw [← add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A))

Tactic:
simp [u.prop]

Premises used: Subtype.prop
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
simp :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      ((z.im * w.im) • HSMul.hSMul (β := A) a 1 + (z.im * w.im) • b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)

Tactic:
simp only [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      ((z.im * w.im) • HSMul.hSMul (β := A) a 1 + (z.im * w.im) • b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)

Tactic:
module
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
u₁ :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₂ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₃ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A))
u₄ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
u₅ :
  HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)

Tactic:
calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp

Premises used: QuadraticAlgebra.re, HMul.hMul, HAdd.hAdd, QuadraticAlgebra.im, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := A) (re (a := a) (b := b) 0) 1 +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (im (a := a) (b := b) 0) (↑u : A) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
simp :
  HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) + w.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)
⊢ HSMul.hSMul (β := A) (z + w).re 1 + (z + w).im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A))

Tactic:
simp only [re_add, im_add, add_smul, ← add_assoc]

Premises used: add_assoc, add_smul, QuadraticAlgebra.re_add, QuadraticAlgebra.im_add
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a :
  HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
⊢ HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) + w.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)

Tactic:
congr 1
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a :
  HSMul.hSMul (β := A) z.re 1 + (HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A)) =
    HSMul.hSMul (β := A) z.re 1 + (z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1)
⊢ HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1

Tactic:
simp only [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a : HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
⊢ HSMul.hSMul (β := A) z.re 1 + (HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A)) =
    HSMul.hSMul (β := A) z.re 1 + (z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1)

Tactic:
congr 1
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
e_a e_a₁ : z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
⊢ HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1

Tactic:
rw [add_comm]

Premises used: add_comm