awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
rw₁ :
  HMul.hMul (α := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      (z * star z) =
    1
rw₂ :
  HMul.hMul (α := QuadraticAlgebra K a b) (β := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z) :
        QuadraticAlgebra K a b) =
    1
rw₃ :
  Eq (α := QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        (HMul.hMul (α := K) (β := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K)
          ((norm : (a : QuadraticAlgebra K a b) → K) z : K)) :
      QuadraticAlgebra K a b)
    (1 : QuadraticAlgebra K a b)
rw₄ :
  Eq (α := QuadraticAlgebra K a b) ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b) 1) 1
rw₅ rw₆ : Eq.{u_1 + 1} (α := QuadraticAlgebra K a b) 1 1
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1

Tactic:
rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]

Premises used: QuadraticAlgebra.C_eq_algebraMap, QuadraticAlgebra.C_mul_eq_smul, map_mul, map_one, QuadraticAlgebra.algebraMap_norm_eq_mul_star, inv_mul_cancel₀
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
re : Eq.{u_1 + 1} (α := K) (QuadraticAlgebra.re (a := a) (b := b) 0⁻¹) (QuadraticAlgebra.re (a := a) (b := b) 0)
im : Eq.{u_1 + 1} (α := K) (QuadraticAlgebra.im (a := a) (b := b) 0⁻¹) (QuadraticAlgebra.im (a := a) (b := b) 0)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra K a b) 0⁻¹ 0

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
⊢ Eq.{u_1 + 1} (α := K) (re (a := a) (b := b) 0⁻¹) (re (a := a) (b := b) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
⊢ Eq.{u_1 + 1} (α := K) (im (a := a) (b := b) 0⁻¹) (im (a := a) (b := b) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
re :
  QuadraticAlgebra.re (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).im
⊢ (↑q : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
re : (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
⊢ QuadraticAlgebra.re (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).re

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
⊢ im (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).im

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
re : (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))

Tactic:
field_simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
⊢ (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
simp [NNRat.cast_def]

Premises used: NNRat.cast_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
re : (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re
im : (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im
⊢ q • x = (↑q : QuadraticAlgebra K a b) * x

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re

Tactic:
simp [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im

Tactic:
simp [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
re :
  QuadraticAlgebra.re (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).im
⊢ (↑q : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
re : (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
⊢ QuadraticAlgebra.re (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).re

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
⊢ im (a := a) (b := b) (↑q : QuadraticAlgebra K a b) =
    (HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)).im

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
re : (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))

Tactic:
field_simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
⊢ (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
simp [Rat.cast_def]

Premises used: Rat.cast_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
re : (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re
im : (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im
⊢ q • x = (↑q : QuadraticAlgebra K a b) * x

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re

Tactic:
simp [Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im

Tactic:
simp [Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
z : QuadraticAlgebra R a b
⊢ { re := z.re, im := z.im } = z

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 : Subsingleton R
⊢ Subsingleton.{u_1 + 1} (QuadraticAlgebra R a b)

Tactic:
(equivProd a b).subsingleton

Premises used: QuadraticAlgebra.equivProd, Equiv.subsingleton
-- 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 : Nontrivial R
⊢ Nontrivial.{u_1} (QuadraticAlgebra R a b)

Tactic:
(equivProd a b).nontrivial

Premises used: Equiv.nontrivial, QuadraticAlgebra.equivProd
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b r : R
inst : Zero R
⊢ re (a := a) (b := b) (QuadraticAlgebra.C r) = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b r : R
inst : Zero R
⊢ im (a := a) (b := b) (QuadraticAlgebra.C r) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := QuadraticAlgebra R a b) QuadraticAlgebra.C

Tactic:
fun _ _ h => congr_arg re h

Premises used: QuadraticAlgebra.re, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
x y : R
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y) ↔ x = y

Tactic:
C_injective.eq_iff

Premises used: Function.Injective.eq_iff, QuadraticAlgebra.C_injective
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) 0) 0

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: QuadraticAlgebra.C, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
r : R
rw : Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) (QuadraticAlgebra.C 0) ↔ r = 0
rw₁ rw₂ : r = 0 ↔ r = 0
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 0 ↔ r = 0

Tactic:
rw [← C_zero, C_inj]

Premises used: QuadraticAlgebra.C_inj, QuadraticAlgebra.C_zero
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
inst_1 : One R
⊢ Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) 1) 1

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: QuadraticAlgebra.C, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Zero R
inst_1 : One R
r : R
rw : Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) (QuadraticAlgebra.C 1) ↔ r = 1
rw₁ rw₂ : r = 1 ↔ r = 1
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 1 ↔ r = 1

Tactic:
rw [← C_one, C_inj]

Premises used: QuadraticAlgebra.C_one, QuadraticAlgebra.C_inj
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Add R
z w : QuadraticAlgebra R a b
⊢ (z + w).re = z.re + w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Add R
z w : QuadraticAlgebra R a b
⊢ (z + w).im = z.im + w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Add R
z w : QuadraticAlgebra R a b
⊢ HAdd.hAdd (α := QuadraticAlgebra R a b) { re := z.re, im := z.im : QuadraticAlgebra R a b }
      { re := w.re, im := w.im : QuadraticAlgebra R a b } =
    { re := z.re + w.re, im := z.im + w.im }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : AddZeroClass R
x y : R
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).re
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).im
⊢ QuadraticAlgebra.C (x + y) = HAdd.hAdd (α := 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 : AddZeroClass R
x y : R
⊢ re (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
    (HAdd.hAdd (α := 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 : AddZeroClass R
x y : R
⊢ im (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Neg R
z : QuadraticAlgebra R a b
⊢ (-z).re = -z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Neg R
z : QuadraticAlgebra R a b
⊢ (-z).im = -z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Neg R
x y : R
⊢ Eq (α := QuadraticAlgebra R a b) (-{ re := x, im := y }) { re := -x, im := -y }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NegZeroClass R
x : R
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (-x)) =
    QuadraticAlgebra.re (a := a) (b := b) (-QuadraticAlgebra.C x)
im :
  QuadraticAlgebra.im (a := a) (b := b) (QuadraticAlgebra.C (-x)) =
    QuadraticAlgebra.im (a := a) (b := b) (-QuadraticAlgebra.C x)
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (-x)) (-QuadraticAlgebra.C x)

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : NegZeroClass R
x : R
⊢ re (a := a) (b := b) (QuadraticAlgebra.C (-x)) = re (a := a) (b := b) (-QuadraticAlgebra.C x)

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

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Sub R
z w : QuadraticAlgebra R a b
⊢ (z - w).re = z.re - w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Sub R
z w : QuadraticAlgebra R a b
⊢ (z - w).im = z.im - w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Sub R
x1 y1 x2 y2 : R
⊢ HSub.hSub (α := QuadraticAlgebra R a b) { re := x1, im := y1 : QuadraticAlgebra R a b }
      { re := x2, im := y2 : QuadraticAlgebra R a b } =
    { re := x1 - x2, im := y1 - y2 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b r1 r2 : R
inst : SubNegZeroMonoid R
⊢ QuadraticAlgebra.C (r1 - r2) = HSub.hSub (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r1) (QuadraticAlgebra.C r2)

Tactic:
QuadraticAlgebra.ext rfl zero_sub_zero.symm

Premises used: QuadraticAlgebra.ext, zero_sub_zero, Eq.symm, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Mul R
inst_1 : Add R
z w : QuadraticAlgebra R a b
⊢ (z * w).re = z.re * w.re + a * z.im * w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Mul R
inst_1 : Add R
z w : QuadraticAlgebra R a b
⊢ (z * w).im = z.re * w.im + z.im * w.re + b * z.im * w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : Mul R
inst_1 : Add R
x1 y1 x2 y2 : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) { re := x1, im := y1 : QuadraticAlgebra R a b }
      { re := x2, im := y2 : QuadraticAlgebra R a b } =
    { re := x1 * x2 + a * y1 * y2, im := x1 * y2 + y1 * x2 + b * y1 * y2 }

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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
re : ((s • t) • z).re = (s • t • z).re
im : ((s • t) • z).im = (s • t • z).im
⊢ (s • t) • z = s • t • z

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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).re = (s • t • z).re

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).re = (s • t • z).re

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).im = (s • t • z).im

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).im = (s • t • z).im

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
re : (s • t • z).re = (t • s • z).re
im : (s • t • z).im = (t • s • z).im
⊢ s • t • z = t • s • z

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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).re = (t • s • z).re

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).re = (t • s • z).re

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).im = (t • s • z).im

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).im = (t • s • z).im

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
re : (MulOpposite.op s • z).re = (s • z).re
im : (MulOpposite.op s • z).im = (s • z).im
⊢ MulOpposite.op s • z = s • z

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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).re = (s • z).re

Tactic:
op_smul_eq_smul _ _

Premises used: IsCentralScalar.op_smul_eq_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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).re = (s • z).re

Tactic:
exact op_smul_eq_smul _ _

Premises used: IsCentralScalar.op_smul_eq_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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).im = (s • z).im

Tactic:
op_smul_eq_smul _ _

Premises used: IsCentralScalar.op_smul_eq_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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul.{u_2, u_1} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).im = (s • z).im

Tactic:
exact op_smul_eq_smul _ _

Premises used: IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
a b : R
inst : SMul S R
s : S
z : QuadraticAlgebra R a b
⊢ (s • z).re = s • z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
a b : R
inst : SMul S R
s : S
z : QuadraticAlgebra R a b
⊢ (s • z).im = s • z.im

Tactic:
rfl

Premises used: rfl