awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)
have re : 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: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ (↑q : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)
have im : 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: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 (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
have re : (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
Tactic: simp [sq]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
have re : (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 = (↑q : QuadraticAlgebra K a b) * x
have re : (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ q • x = (↑q : QuadraticAlgebra K a b) * x
have im : (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)
have re : 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: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ (↑q : QuadraticAlgebra K a b) =
    HDiv.hDiv (α := QuadraticAlgebra K a b) (↑q.num : QuadraticAlgebra K a b) (↑q.den : QuadraticAlgebra K a b)
have im : 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: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 (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
have re : (↑q : K) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
Tactic: simp [sq]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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) = (↑q.num : K) * (HMul.hMul (α := K) (↑q.den : K)⁻¹ (↑q.den : K)⁻¹ * (↑q.den : K))
have re : (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 = (↑q : QuadraticAlgebra K a b) * x
have re : (q • x).re = ((↑q : QuadraticAlgebra K a b) * x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ q • x = (↑q : QuadraticAlgebra K a b) * x
have im : (q • x).im = ((↑q : QuadraticAlgebra K a b) * x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : Zero R
r : R
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 0 ↔ r = 0
have rw : Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) (QuadraticAlgebra.C 0) ↔ r = 0
Tactic: rw [← C_zero, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 0 ↔ r = 0
have rw₁ : r = 0 ↔ r = 0
Tactic: rw [← C_zero, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : Zero R
inst_1 : One R
r : R
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 1 ↔ r = 1
have rw : Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) (QuadraticAlgebra.C 1) ↔ r = 1
Tactic: rw [← C_one, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) 1 ↔ r = 1
have rw₁ : r = 1 ↔ r = 1
Tactic: rw [← C_one, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : AddZeroClass R
x y : R
⊢ QuadraticAlgebra.C (x + y) = HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)
have re : re (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
  (HAdd.hAdd (α := 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 : 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
⊢ QuadraticAlgebra.C (x + y) = HAdd.hAdd (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C x) (QuadraticAlgebra.C y)
have im : im (a := a) (b := b) (QuadraticAlgebra.C (x + y)) =
  (HAdd.hAdd (α := 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
a b : R
inst : NegZeroClass R
x : R
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (-x)) (-QuadraticAlgebra.C x)
have re : re (a := a) (b := b) (QuadraticAlgebra.C (-x)) = re (a := a) (b := b) (-QuadraticAlgebra.C x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
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)
⊢ Eq (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (-x)) (-QuadraticAlgebra.C x)
have im : im (a := a) (b := b) (QuadraticAlgebra.C (-x)) = im (a := a) (b := b) (-QuadraticAlgebra.C x)
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 : 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 = s • t • z
have re : ((s • t) • z).re = (s • t • z).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 : 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
⊢ (s • t) • z = s • t • z
have im : ((s • t) • z).im = (s • t • z).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 : 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 = t • s • z
have re : (s • t • z).re = (t • s • z).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 : 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
⊢ s • t • z = t • s • z
have im : (s • t • z).im = (t • s • z).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 : 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 = s • z
have re : (MulOpposite.op s • z).re = (s • z).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 : 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
⊢ MulOpposite.op s • z = s • z
have im : (MulOpposite.op s • z).im = (s • z).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 : Monoid S
inst_1 : MulAction S R
x_1 x_2 : S
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 : 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
⊢ (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 : 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 = x_1
have re : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 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 : 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
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := S) 1 x_1 = x_1
have im : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 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 : AddMonoid R
⊢ AddMonoid (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_
-- 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 : 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)
⊢ AddMonoid (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_
-- 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 : Monoid S
inst_1 : AddMonoid R
inst_2 : DistribMulAction S R
x_1 : S
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) x_1 0 = 0
have re : (HSMul.hSMul (β := QuadraticAlgebra R a b) 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 : 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
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) x_1 0 = 0
have im : (HSMul.hSMul (β := QuadraticAlgebra R a b) 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
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) = 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 : 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
⊢ 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 : AddCommMonoid R
⊢ AddCommMonoid (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_
-- 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 : 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)
⊢ AddCommMonoid (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_
-- 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_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 = r • x + s • x
have re : ((r + s) • x).re = (r • x + s • x).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_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
⊢ (r + s) • x = r • x + s • x
have im : ((r + s) • x).im = (r • x + s • x).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_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 = 0
have re : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).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_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
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x = 0
have im : (HSMul.hSMul.{u_2, u_1, u_1} (α := S) 0 x).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 : AddGroup R
⊢ AddGroup (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_
-- 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 : 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)
⊢ AddGroup (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_
-- 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 : 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)
⊢ AddGroup (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_
-- 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 : 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)
⊢ AddGroup (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_
-- 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 : 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)
⊢ AddGroup (QuadraticAlgebra R a b)
have 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)
Tactic: refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_
-- 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
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C (↑0 : R)) 0
have re : Eq.{u_1 + 1} (α := R) (re (a := a) (b := b) (QuadraticAlgebra.C (↑0 : R))) (re (a := a) (b := b) 0)
Tactic: ext