awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑0 : R)) 0
have im : Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R))) (im (a := a) (b := b) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 : ℕ
⊢ QuadraticAlgebra.C (↑(n + 1) : R) = HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1
have re : re (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
  (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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
⊢ QuadraticAlgebra.C (↑(n + 1) : R) = HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1
have im : im (a := a) (b := b) (QuadraticAlgebra.C (↑(n + 1) : R)) =
  (HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) 1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : AddCommMonoidWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (OfNat.ofNat n)) (OfNat.ofNat n)
have re : Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n))) (re (a := a) (b := b) (OfNat.ofNat n))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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))
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (OfNat.ofNat n)) (OfNat.ofNat n)
have im : Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C (OfNat.ofNat n))) (im (a := a) (b := b) (OfNat.ofNat n))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑(↑n : ℤ) : R)) (↑n : QuadraticAlgebra R a b)
have norm_cast : Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑n : R)) (↑n : QuadraticAlgebra R a b)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑(Int.negSucc n) : R))
    (-(↑(n + 1) : QuadraticAlgebra R a b))
have rw : Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R))
  (-(↑(n + 1) : QuadraticAlgebra R a b))
Tactic: rw [Int.negSucc_eq, Int.cast_neg, C_neg]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R))
    (-(↑(n + 1) : QuadraticAlgebra R a b))
have norm_cast : Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (-QuadraticAlgebra.C (↑(n + 1) : R)) (-(↑(n + 1) : QuadraticAlgebra R a b))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have im : (x_1 * (x_2 + x_3)).im = (x_1 * x_2 + x_1 * x_3).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
have 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)
Tactic: simp [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 * (x_2 + x_3)).im = (x_1 * x_2 + x_1 * x_3).im
have 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)
Tactic: simp [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have im : ((x_1 + x_2) * x_3).im = (x_1 * x_3 + x_2 * x_3).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
have 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)
Tactic: simp [mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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 + x_2) * x_3).im = (x_1 * x_3 + x_2 * x_3).im
have 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)
Tactic: simp [mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonUnitalNonAssocSemiring R
x_1 : QuadraticAlgebra R a b
⊢ 0 * x_1 = 0
have re : (0 * x_1).re = re (a := a) (b := b) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonUnitalNonAssocSemiring R
x_1 : QuadraticAlgebra R a b
re : (0 * x_1).re = QuadraticAlgebra.re (a := a) (b := b) 0
⊢ 0 * x_1 = 0
have im : (0 * x_1).im = im (a := a) (b := b) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonUnitalNonAssocSemiring R
x_1 : QuadraticAlgebra R a b
⊢ x_1 * 0 = 0
have re : (x_1 * 0).re = re (a := a) (b := b) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonUnitalNonAssocSemiring R
x_1 : QuadraticAlgebra R a b
re : (x_1 * 0).re = QuadraticAlgebra.re (a := a) (b := b) 0
⊢ x_1 * 0 = 0
have im : (x_1 * 0).im = im (a := a) (b := b) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ QuadraticAlgebra.C r * x = r • x
have re : (QuadraticAlgebra.C r * x).re = (r • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
re : (QuadraticAlgebra.C r * x).re = (r • x).re
⊢ QuadraticAlgebra.C r * x = r • x
have im : (QuadraticAlgebra.C r * x).im = (r • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ QuadraticAlgebra.C (x * y) = HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)
have re : re (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
  (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalNonAssocSemiring R
x y : R
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).re
⊢ QuadraticAlgebra.C (x * y) = HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)
have im : im (a := a) (b := b) (QuadraticAlgebra.C (x * y)) =
  (HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonAssocSemiring R
x_1 : QuadraticAlgebra R a b
⊢ 1 * x_1 = x_1
have re : (1 * x_1).re = x_1.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonAssocSemiring R
x_1 : QuadraticAlgebra R a b
re : (1 * x_1).re = x_1.re
⊢ 1 * x_1 = x_1
have im : (1 * x_1).im = x_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonAssocSemiring R
x_1 : QuadraticAlgebra R a b
⊢ x_1 * 1 = x_1
have re : (x_1 * 1).re = x_1.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : NonAssocSemiring R
x_1 : QuadraticAlgebra R a b
re : (x_1 * 1).re = x_1.re
⊢ x_1 * 1 = x_1
have im : (x_1 * 1).im = x_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonAssocSemiring R
n : ℕ
x y : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b } =
    { re := (↑n : R) * x, im := (↑n : R) * y }
have re : (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
      { re := x, im := y : QuadraticAlgebra R a b }).re =
  re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : NonAssocSemiring R
n : ℕ
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b } =
    { re := (↑n : R) * x, im := (↑n : R) * y }
have im : (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
      { re := x, im := y : QuadraticAlgebra R a b }).im =
  im (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)
have re : (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
re : (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)
have im : (x_1 * x_2 * x_3).im = (x_1 * (x_2 * x_3)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re
have re : (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.re +
    a * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
  x_1.re * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
    a * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 x_3 : QuadraticAlgebra R a b
⊢ (x_1 * x_2 * x_3).im = (x_1 * (x_2 * x_3)).im
have im : (x_1.re * x_2.re + a * x_1.im * x_2.im) * x_3.im + (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.re +
    b * (x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im) * x_3.im =
  x_1.re * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im) +
      x_1.im * (x_2.re * x_3.re + a * x_2.im * x_3.im) +
    b * x_1.im * (x_2.re * x_3.im + x_2.im * x_3.re + b * x_2.im * x_3.im)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 : QuadraticAlgebra R a b
⊢ x_1 * x_2 = x_2 * x_1
have re : (x_1 * x_2).re = (x_2 * x_1).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 : QuadraticAlgebra R a b
re : (x_1 * x_2).re = (x_2 * x_1).re
⊢ x_1 * x_2 = x_2 * x_1
have im : (x_1 * x_2).im = (x_2 * x_1).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 : QuadraticAlgebra R a b
⊢ (x_1 * x_2).re = (x_2 * x_1).re
have re : x_1.re * x_2.re + a * x_1.im * x_2.im = x_2.re * x_1.re + a * x_2.im * x_1.im
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
x_1 x_2 : QuadraticAlgebra R a b
⊢ (x_1 * x_2).im = (x_2 * x_1).im
have im : x_1.re * x_2.im + x_1.im * x_2.re + b * x_1.im * x_2.im = x_2.re * x_1.im + x_2.im * x_1.re + b * x_2.im * x_1.im
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1) : QuadraticAlgebra R a b) (1 : QuadraticAlgebra R a b)
have re : Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
  (re (a := a) (b := b) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
re :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
    (QuadraticAlgebra.re (a := a) (b := b) 1 : R)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1) : QuadraticAlgebra R a b) (1 : QuadraticAlgebra R a b)
have im : Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 1)) : R)
  (im (a := a) (b := b) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y)) =
    HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)
have re : re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y)) =
    HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)
have im : im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x * y))) =
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0) : QuadraticAlgebra R a b) (0 : QuadraticAlgebra R a b)
have re : Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
  (re (a := a) (b := b) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
re :
  Eq.{u_1 + 1} (α := R)
    (QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
    (QuadraticAlgebra.re (a := a) (b := b) 0 : R)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0) : QuadraticAlgebra R a b) (0 : QuadraticAlgebra R a b)
have im : Eq.{u_1 + 1} (α := R) (im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) 0)) : R)
  (im (a := a) (b := b) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y)) =
    HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)
have re : re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
  (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y_1 : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
re :
  QuadraticAlgebra.re (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
    (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
        (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).re
⊢ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y)) =
    HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)
have im : im (a := a) (b := b) (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) (x + y))) =
  (HAdd.hAdd (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) x) : QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) y) : QuadraticAlgebra R a b)).im
Tactic: ext