awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 }
r : R
⊢ HSMul.hSMul (β := A) (re (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r))
        1 +
      im (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r) • (↑u : A) =
    (algebraMap R A : (a : R) → A) r

Tactic:
simp [← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- 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
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ HMul.hMul (α := A) (β := A) ((f : (a : QuadraticAlgebra R a b) → A) ω : A)
      ((f : (a : QuadraticAlgebra R a b) → A) ω : A) =
    HSMul.hSMul (β := A) a 1 + HSMul.hSMul (β := A) b ((f : (a : QuadraticAlgebra R a b) → A) ω : A)

Tactic:
simp [← map_mul, omega_mul_omega_eq_add]

Premises used: map_mul, QuadraticAlgebra.omega_mul_omega_eq_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
r : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
⊢ (fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
        (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
            ((f : (a : QuadraticAlgebra R a b) → A) ω) ⋯ :
          { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
      ((fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
          ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
            QuadraticAlgebra R a b →ₐ[R] A))
        r) =
    r

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
f : QuadraticAlgebra R a b →ₐ[R] A
h :
  Eq.{u_3 + 1} (α := A)
    (((fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
              ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A),
                  map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
                QuadraticAlgebra R a b →ₐ[R] A))
            ((fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
                (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
                    ((f : (a : QuadraticAlgebra R a b) → A) ω) ⋯ :
                  { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
              f) :
          (a : QuadraticAlgebra R a b) → A)
        ω :
      A)
    ((f : (a : QuadraticAlgebra R a b) → A) ω : A)
⊢ (fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
        ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A), map_one' := ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
          QuadraticAlgebra R a b →ₐ[R] A))
      ((fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
          (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
              ((f : (a : QuadraticAlgebra R a b) → A) ω) ⋯ :
            { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
        f) =
    f

Tactic:
ext
-- 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
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ Eq.{u_3 + 1} (α := A)
    (((fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
              ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A),
                  map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
                QuadraticAlgebra R a b →ₐ[R] A))
            ((fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
                (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
                    ((f : (a : QuadraticAlgebra R a b) → A) ω) ⋯ :
                  { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
              f) :
          (a : QuadraticAlgebra R a b) → A)
        ω :
      A)
    ((f : (a : QuadraticAlgebra R a b) → A) ω : A)

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ (star z).re = z.re + b * z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ (star z).im = -z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x y : R
re : x * (x + b * y) + -(a * y * y) = x * x + b * x * y - a * y * y
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
        (star { re := x, im := y : QuadraticAlgebra R a b })).re =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
          HMul.hMul (β := QuadraticAlgebra R a b)
            (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)).re

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

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

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 0

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ (star (star x)).re = x.re

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ star (star x) = x

Tactic:
refine QuadraticAlgebra.ext (by simp) (neg_neg _)

Premises used: QuadraticAlgebra.ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : CommRing R
a b : QuadraticAlgebra R a_1 b_1
re : (star (a * b)).re = (star b * star a).re
im : (star (a * b)).im = (star b * star a).im
⊢ star (a * b) = star b * star a

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : CommRing R
a b : QuadraticAlgebra R a_1 b_1
re :
  a.re * b.re + a_1 * a.im * b.im + b_1 * (a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
    (b.re + b_1 * b.im) * (a.re + b_1 * a.im) + a_1 * b.im * a.im
⊢ (star (a * b)).re = (star b * star a).re

Tactic:
simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]

Premises used: neg_neg, QuadraticAlgebra.re_star, QuadraticAlgebra.im_mul, neg_mul, QuadraticAlgebra.re_mul, QuadraticAlgebra.im_star, mul_neg
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : CommRing R
a b : QuadraticAlgebra R a_1 b_1
im :
  -(a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
    -((b.re + b_1 * b.im) * a.im) + -(b.im * (a.re + b_1 * a.im)) + b_1 * b.im * a.im
⊢ (star (a * b)).im = (star b * star a).im

Tactic:
simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]

Premises used: neg_neg, QuadraticAlgebra.re_star, QuadraticAlgebra.im_mul, neg_mul, QuadraticAlgebra.re_mul, QuadraticAlgebra.im_star, mul_neg
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : CommRing R
a b : QuadraticAlgebra R a_1 b_1
⊢ a.re * b.re + a_1 * a.im * b.im + b_1 * (a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
    (b.re + b_1 * b.im) * (a.re + b_1 * a.im) + a_1 * b.im * a.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : CommRing R
a b : QuadraticAlgebra R a_1 b_1
⊢ -(a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
    -((b.re + b_1 * b.im) * a.im) + -(b.im * (a.re + b_1 * a.im)) + b_1 * b.im * a.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
x x_1 : QuadraticAlgebra R a b
simp : x.re + x_1.re + b * (x.im + x_1.im) = x.re + b * x.im + (x_1.re + b * x_1.im)
⊢ (star (x + x_1)).re = (star x + star x_1).re

Tactic:
simp only [re_star, re_add, im_add]

Premises used: QuadraticAlgebra.re_star, QuadraticAlgebra.re_add, QuadraticAlgebra.im_add
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
x x_1 : QuadraticAlgebra R a b
⊢ x.re + x_1.re + b * (x.im + x_1.im) = x.re + b * x.im + (x_1.re + b * x_1.im)

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
⊢ HMul.hMul (α := R) (re (a := a) (b := b) 1) (re (a := a) (b := b) 1) +
        b * re (a := a) (b := b) 1 * im (a := a) (b := b) 1 -
      a * im (a := a) (b := b) 1 * im (a := a) (b := b) 1 =
    1

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
z w : QuadraticAlgebra R a b
simp :
  (z.re * w.re + a * z.im * w.im) * (z.re * w.re + a * z.im * w.im) +
        b * (z.re * w.re + a * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) -
      a * (z.re * w.im + z.im * w.re + b * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)
⊢ (z * w).re * (z * w).re + b * (z * w).re * (z * w).im - a * (z * w).im * (z * w).im =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)

Tactic:
simp only [re_mul, im_mul]

Premises used: QuadraticAlgebra.im_mul, QuadraticAlgebra.re_mul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re + a * z.im * w.im) * (z.re * w.re + a * z.im * w.im) +
        b * (z.re * w.re + a * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) -
      a * (z.re * w.im + z.im * w.re + b * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ (norm : (a : QuadraticAlgebra R a b) → R) z = z.re * z.re + b * z.re * z.im - a * z.im * z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
⊢ Eq.{u_2 + 1} (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) 0 : R) (0 : R)

Tactic:
simp [norm]

Premises used: QuadraticAlgebra.norm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
⊢ Eq.{u_2 + 1} (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) 1 : R) (1 : R)

Tactic:
simp [norm]

Premises used: QuadraticAlgebra.norm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
⊢ (norm : (a : QuadraticAlgebra R a b) → R)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    HPow.hPow (β := ℕ) r 2

Tactic:
simp [norm_def, pow_two]

Premises used: pow_two, QuadraticAlgebra.norm_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
n : ℕ
⊢ (norm : (a : QuadraticAlgebra R a b) → R) (↑n : QuadraticAlgebra R a b) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2

Tactic:
simp [norm_def, pow_two]

Premises used: pow_two, QuadraticAlgebra.norm_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
n : ℤ
⊢ (norm : (a : QuadraticAlgebra R a b) → R) (↑n : QuadraticAlgebra R a b) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2

Tactic:
simp [norm_def, pow_two]

Premises used: pow_two, QuadraticAlgebra.norm_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
re :
  QuadraticAlgebra.re (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).re
im :
  QuadraticAlgebra.im (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).im
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
      ((norm : (a : QuadraticAlgebra R a b) → R) z) =
    z * star z

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
re : 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))
⊢ QuadraticAlgebra.re (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).re

Tactic:
simp [norm, star, mul_comm]

Premises used: QuadraticAlgebra.norm, mul_comm, Star.star
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
im : 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))
⊢ QuadraticAlgebra.im (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).im

Tactic:
simp [norm, star, mul_comm]

Premises used: QuadraticAlgebra.norm, mul_comm, Star.star
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
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))

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
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:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) (-x) : R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)

Tactic:
simp [norm]

Premises used: QuadraticAlgebra.norm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
simp : (x.re + b * x.im) * (x.re + b * x.im) + -(b * (x.re + b * x.im) * x.im) = x.re * x.re + b * x.re * x.im
⊢ Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) (star x) : R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)

Tactic:
simp only [norm, MonoidHom.coe_mk, OneHom.coe_mk, re_star, im_star, mul_neg, neg_mul, neg_neg,
    sub_left_inj]

Premises used: OneHom.coe_mk, neg_neg, sub_left_inj, QuadraticAlgebra.re_star, QuadraticAlgebra.norm, MonoidHom.coe_mk, neg_mul, QuadraticAlgebra.im_star, mul_neg
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ (x.re + b * x.im) * (x.re + b * x.im) + -(b * (x.re + b * x.im) * x.im) = x.re * x.re + b * x.re * x.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
mp : IsUnit x → IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
mpr : IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) → IsUnit x
⊢ IsUnit x ↔ IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)

Tactic:
constructor
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit x → IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)

Tactic:
IsUnit.map norm

Premises used: QuadraticAlgebra.norm, IsUnit.map
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit x → IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)

Tactic:
exact IsUnit.map norm

Premises used: QuadraticAlgebra.norm, IsUnit.map
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
mpr :
  (∃ (b_1 : R),
      HMul.hMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) b_1 = 1 ∧
        HMul.hMul (β := R) b_1 ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1) →
    ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1
⊢ IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) → IsUnit x

Tactic:
simp only [isUnit_iff_exists]

Premises used: isUnit_iff_exists
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : HMul.hMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) r = 1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
⊢ x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1

Tactic:
rw [← C_inj (R := R) (a := a) (b := b), C_mul, C_eq_algebraMap, algebraMap_norm_eq_mul_star,
      mul_assoc, map_one] at hr

Premises used: QuadraticAlgebra.C_eq_algebraMap, mul_assoc, QuadraticAlgebra.C_mul, map_one, QuadraticAlgebra.algebraMap_norm_eq_mul_star, QuadraticAlgebra.C_inj
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : HMul.hMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) r = 1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
hr₁ :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
⊢ HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1

Tactic:
rw [← C_inj (R := R) (a := a) (b := b), C_mul, C_eq_algebraMap, algebraMap_norm_eq_mul_star,
      mul_assoc, map_one] at hr

Premises used: QuadraticAlgebra.C_eq_algebraMap, mul_assoc, QuadraticAlgebra.C_mul, map_one, QuadraticAlgebra.algebraMap_norm_eq_mul_star, QuadraticAlgebra.C_inj
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
⊢ ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
⟨_, hr, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
mpr :
  HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) *
      x =
    1
⊢ ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
refine ⟨_, hr, ?_⟩
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
mpr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
mpr₁ mpr₂ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 1 1
⊢ HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) *
      x =
    1

Tactic:
rw [mul_comm, hr]

Premises used: mul_comm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
rw :
  Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) (1 : R) ↔
    Eq (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
          ((norm : (a : QuadraticAlgebra R a b) → R) z) :
        QuadraticAlgebra R a b)
      (1 : QuadraticAlgebra R a b)
⊢ Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) (1 : R) ↔
    Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (unitary (QuadraticAlgebra R a b)) z

Tactic:
rw [Unitary.mem_iff_self_mul_star, ← algebraMap_norm_eq_mul_star]

Premises used: Unitary.mem_iff_self_mul_star, QuadraticAlgebra.algebraMap_norm_eq_mul_star