awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
a b : R
inst : SMul S R
s : S
x y : R
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) s { re := x, im := y : QuadraticAlgebra R a b } =
    { re := s • x, im := s • y }

Tactic:
rfl

Premises used: 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 : Monoid S
inst_1 : MulAction S R
x_1 x_2 : S
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 : Monoid S
inst_1 : MulAction S R
x_1 x_2 : S
x_3 : QuadraticAlgebra R a b
⊢ ((x_1 * x_2) • x_3).re = (x_1 • x_2 • x_3).re

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- 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 : Monoid S
inst_1 : MulAction S R
x_1 x_2 : S
x_3 : QuadraticAlgebra R a b
⊢ ((x_1 * x_2) • x_3).im = (x_1 • x_2 • x_3).im

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- 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 : Monoid S
inst_1 : MulAction S R
x_1 : QuadraticAlgebra R a b
re : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 1 x_1).re = x_1.re
im : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 1 x_1).im = x_1.im
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := S) 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 : Monoid S
inst_1 : MulAction S R
x_1 : QuadraticAlgebra R a b
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 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 : Monoid S
inst_1 : MulAction S R
x_1 : QuadraticAlgebra R a b
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 1 x_1).im = x_1.im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
a b : R
inst : Zero R
inst_1 : SMulZeroClass S R
s : S
r : R
⊢ QuadraticAlgebra.C (s • r) = HSMul.hSMul (β := QuadraticAlgebra R a b) s (QuadraticAlgebra.C r)

Tactic:
QuadraticAlgebra.ext rfl (smul_zero _).symm

Premises used: QuadraticAlgebra.ext, smul_zero, Eq.symm, 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 : AddMonoid R
refine_1 :
  ∀ (x y : QuadraticAlgebra R a b),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x + y) =
      HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
        ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y : R × R)
refine_2 :
  ∀ (x : QuadraticAlgebra R a b) (n : ℕ),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x) =
      HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
⊢ AddMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_

Premises used: Function.Injective.addMonoid, QuadraticAlgebra.equivProd, Equiv.injective, 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 : AddMonoid R
x_1 y_1 : QuadraticAlgebra R a b
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x_1 + y_1) =
    HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)
      ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y_1 : R × R)

Tactic:
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 : AddMonoid R
x_1 : QuadraticAlgebra R a b
n : ℕ
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x_1) =
    HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)

Tactic:
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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
re : (HSMul.hSMul (β := QuadraticAlgebra R a b) x_1 0).re = QuadraticAlgebra.re (a := a) (b := b) 0
im : (HSMul.hSMul (β := QuadraticAlgebra R a b) x_1 0).im = QuadraticAlgebra.im (a := a) (b := b) 0
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) 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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
⊢ (HSMul.hSMul (β := 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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
⊢ (HSMul.hSMul (β := 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
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
x_2 x_3 : QuadraticAlgebra R a b
re : (x_1 • (x_2 + x_3)).re = (x_1 • x_2 + x_1 • x_3).re
im : (x_1 • (x_2 + x_3)).im = (x_1 • x_2 + x_1 • x_3).im
⊢ x_1 • (x_2 + x_3) = x_1 • x_2 + x_1 • 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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1 • (x_2 + x_3)).re = (x_1 • x_2 + x_1 • 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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1 • (x_2 + x_3)).im = (x_1 • x_2 + x_1 • 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 : AddCommMonoid R
refine_1 :
  ∀ (x y : QuadraticAlgebra R a b),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x + y) =
      HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
        ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y : R × R)
refine_2 :
  ∀ (x : QuadraticAlgebra R a b) (n : ℕ),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x) =
      HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
⊢ AddCommMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_

Premises used: Function.Injective.addCommMonoid, QuadraticAlgebra.equivProd, Equiv.injective, 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 : AddCommMonoid R
x_1 y_1 : QuadraticAlgebra R a b
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x_1 + y_1) =
    HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)
      ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y_1 : R × R)

Tactic:
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 : AddCommMonoid R
x_1 : QuadraticAlgebra R a b
n : ℕ
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x_1) =
    HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)

Tactic:
rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r_1 : R
x_1 y : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
r s : S
x : QuadraticAlgebra R a b
re : ((r + s) • x).re = (r • x + s • x).re
im : ((r + s) • x).im = (r • x + s • x).im
⊢ (r + s) • x = r • x + s • x

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r_1 : R
x_1 y : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).re = (r • x + s • x).re

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r_1 : R
x_1 y : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
x : QuadraticAlgebra R a b
re : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).re = QuadraticAlgebra.re (a := a) (b := b) 0
im : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).im = QuadraticAlgebra.im (a := a) (b := b) 0
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x = 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_1 y : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
x : QuadraticAlgebra R a b
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).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_1 y : QuadraticAlgebra R a b
inst : Semiring S
inst_1 : AddCommMonoid R
inst_2 : Module S R
x : QuadraticAlgebra R a b
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).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 : AddGroup R
refine_1 :
  ∀ (x y : QuadraticAlgebra R a b),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x + y) =
      HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
        ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y : R × R)
refine_2 :
  ∀ (x : QuadraticAlgebra R a b),
    Eq (α := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (-x) : R × R)
      (-(equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
refine_3 :
  ∀ (x y : QuadraticAlgebra R a b),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x - y) =
      HSub.hSub (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
        ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y : R × R)
refine_4 :
  ∀ (x : QuadraticAlgebra R a b) (n : ℕ),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x) =
      HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
refine_5 :
  ∀ (x : QuadraticAlgebra R a b) (n : ℤ),
    (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x) =
      HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x : R × R)
⊢ AddGroup (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_

Premises used: Function.Injective.addGroup, QuadraticAlgebra.equivProd, Equiv.injective, 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 : AddGroup R
x_1 y_1 : QuadraticAlgebra R a b
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x_1 + y_1) =
    HAdd.hAdd (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)
      ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y_1 : R × R)

Tactic:
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 : AddGroup R
x_1 : QuadraticAlgebra R a b
⊢ Eq (α := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (-x_1) : R × R)
    (-(equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)

Tactic:
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 : AddGroup R
x_1 y_1 : QuadraticAlgebra R a b
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (x_1 - y_1) =
    HSub.hSub (α := R × R) (β := R × R) ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)
      ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) y_1 : R × R)

Tactic:
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 : AddGroup R
x_1 : QuadraticAlgebra R a b
n : ℕ
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x_1) =
    HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)

Tactic:
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 : AddGroup R
x_1 : QuadraticAlgebra R a b
n : ℤ
⊢ (equivProd a b : (a : QuadraticAlgebra R a b) → R × R) (n • x_1) =
    HSMul.hSMul (β := R × R) n ((equivProd a b : (a : QuadraticAlgebra R a b) → R × R) x_1 : R × R)

Tactic:
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 : AddCommMonoidWithOne R
re :
  Eq.{u_1 + 1} (α := R) (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R)))
    (QuadraticAlgebra.re (a := a) (b := b) 0)
im :
  Eq.{u_1 + 1} (α := R) (QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R)))
    (QuadraticAlgebra.im (a := a) (b := b) 0)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑0 : R)) 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 : AddCommMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R))) (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 : AddCommMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R))) (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 : AddCommMonoidWithOne R
n : ℕ
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1).im
⊢ QuadraticAlgebra.C (↑(n + 1) : R) = HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 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 : AddCommMonoidWithOne R
n : ℕ
⊢ re (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 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 : AddCommMonoidWithOne R
n : ℕ
⊢ im (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
re :
  Eq.{u_1 + 1} (α := R) (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n)))
    (QuadraticAlgebra.re (a := a) (b := b) (OfNat.ofNat n))
im :
  Eq.{u_1 + 1} (α := R) (QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n)))
    (QuadraticAlgebra.im (a := a) (b := b) (OfNat.ofNat n))
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n)))
    (re (a := a) (b := b) (OfNat.ofNat n))

Tactic:
rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n)))
    (im (a := a) (b := b) (OfNat.ofNat n))

Tactic:
rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (↑n : QuadraticAlgebra R a b)) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (↑n : QuadraticAlgebra R a b)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) (↑n : QuadraticAlgebra R a b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (OfNat.ofNat n)) 0

Tactic:
rfl

Premises used: 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 : AddCommGroupWithOne R
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) (↑n : QuadraticAlgebra R a b)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑(↑n : ℤ) : R)) (↑n : QuadraticAlgebra R a b)

Tactic:
norm_cast
-- 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 : AddCommGroupWithOne R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R))
    (-(↑(n + 1) : QuadraticAlgebra R a b))
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑(Int.negSucc n) : R))
    (-(↑(n + 1) : QuadraticAlgebra R a b))

Tactic:
rw [Int.negSucc_eq, Int.cast_neg, C_neg]

Premises used: Int.cast_neg, QuadraticAlgebra.C_neg, Int.negSucc_eq
-- 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 : AddCommGroupWithOne R
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(n + 1) : R)) (-(↑(n + 1) : QuadraticAlgebra R a b))
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R))
    (-(↑(n + 1) : QuadraticAlgebra R a b))

Tactic:
norm_cast
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommGroupWithOne R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (↑n : QuadraticAlgebra R a b)) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommGroupWithOne R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (↑n : QuadraticAlgebra R a b)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddCommGroupWithOne R
n : ℤ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) (↑n : QuadraticAlgebra R a b)

Tactic:
rfl

Premises used: 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 : NonUnitalNonAssocSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
im : (x_1 * (x_2 + x_3)).im = (x_1 * x_2 + x_1 * x_3).im
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * 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 : NonUnitalNonAssocSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
re :
  x_1.re * x_2.re + x_1.re * x_3.re + (a * x_1.im * x_2.im + a * x_1.im * x_3.im) =
    x_1.re * x_2.re + a * x_1.im * x_2.im + (x_1.re * x_3.re + a * x_1.im * x_3.im)
⊢ (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re

Tactic:
simp [mul_add]

Premises used: mul_add
-- 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
im :
  x_1.re * x_2.im + x_1.re * x_3.im + (x_1.im * x_2.re + x_1.im * x_3.re) +
      (b * x_1.im * x_2.im + b * x_1.im * x_3.im) =
    x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im + (x_1.re * x_3.im + x_1.im * x_3.re + b * x_1.im * x_3.im)
⊢ (x_1 * (x_2 + x_3)).im = (x_1 * x_2 + x_1 * x_3).im

Tactic:
simp [mul_add]

Premises used: mul_add
-- 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_2.re + x_1.re * x_3.re + (a * x_1.im * x_2.im + a * x_1.im * x_3.im) =
    x_1.re * x_2.re + a * x_1.im * x_2.im + (x_1.re * x_3.re + a * x_1.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_2.im + x_1.re * x_3.im + (x_1.im * x_2.re + x_1.im * x_3.re) +
      (b * x_1.im * x_2.im + b * x_1.im * x_3.im) =
    x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im + (x_1.re * x_3.im + x_1.im * x_3.re + b * x_1.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
re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
im : ((x_1 + x_2) * x_3).im = (x_1 * x_3 + x_2 * x_3).im
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + 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 : NonUnitalNonAssocSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
re :
  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)
⊢ ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re

Tactic:
simp [mul_add, add_mul]

Premises used: add_mul, mul_add
-- 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
im :
  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)
⊢ ((x_1 + x_2) * x_3).im = (x_1 * x_3 + x_2 * x_3).im

Tactic:
simp [mul_add, add_mul]

Premises used: add_mul, mul_add