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 b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A) =
    (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A))
have symm : (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
  HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
have simp : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.im * w.re) • (↑u : A) + (z.re * w.im) • (↑u : A) +
    (z.im * w.im) • ((↑u : A) * (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
    (z.im * w.im) • ((↑u : A) * (↑u : A))
Tactic: simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
have e_a : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
have e_a : HSMul.hSMul (β := A) (z.re * w.re) 1 + ((z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
Tactic: simp only [add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + ((z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
have e_a : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A)
Tactic: rw [← add_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
have simp : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
    ((z.im * w.im) • HSMul.hSMul (β := A) a 1 + (z.im * w.im) • b • (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
Tactic: simp only [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
have u₁ : (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
    (z.im * w.im) • ((↑u : A) * (↑u : A))
Tactic: calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
u₁ :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
have u₂ : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
    (z.im * w.im) • ((↑u : A) * (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) + (z.im * w.im) • ((↑u : A) * (↑u : A))
Tactic: calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
u₁ :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₂ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
have u₃ : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) + (z.im * w.im) • ((↑u : A) * (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
    (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A))
Tactic: calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
u₁ :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₂ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₃ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A))
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
have u₄ : HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
    (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A)) =
  HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
Tactic: calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
u₁ :
  (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₂ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im) • (↑u : A) + (z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A))
u₃ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • ((↑u : A) * (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A))
u₄ :
  HSMul.hSMul (β := A) (z.re * w.re) 1 + (z.re * w.im + z.im * w.re) • (↑u : A) +
      (z.im * w.im) • (HSMul.hSMul (β := A) a 1 + b • (↑u : A)) =
    HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A)
⊢ (HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A)) * (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)) =
    HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
have u₅ : HSMul.hSMul (β := A) (z.re * w.re + a * z.im * w.im) 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • (↑u : A) =
  HSMul.hSMul (β := A) (z * w).re 1 + (z * w).im • (↑u : A)
Tactic: calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) (z + w).re 1 + (z + w).im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + (HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A))
have simp : HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) + w.im • (↑u : A) =
  HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)
Tactic: simp only [re_add, im_add, add_smul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) + w.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 + w.im • (↑u : A)
have e_a : HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) =
  HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) z.re 1 + HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) =
    HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
have e_a : HSMul.hSMul (β := A) z.re 1 + (HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A)) =
  HSMul.hSMul (β := A) z.re 1 + (z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1)
Tactic: simp only [add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) z.re 1 + (HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A)) =
    HSMul.hSMul (β := A) z.re 1 + (z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1)
have e_a : HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ HSMul.hSMul (β := A) w.re 1 + z.im • (↑u : A) = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
have e_a : z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1 = z.im • (↑u : A) + HSMul.hSMul (β := A) w.re 1
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ (fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
        ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A), map_one' := ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
          QuadraticAlgebra R a b →ₐ[R] A))
      ((fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
          (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
              ((f : (a : QuadraticAlgebra R a b) → A) ω) ⋯ :
            { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
        f) =
    f
have h : Eq.{u_3 + 1} (α := A)
  (((fun (u : { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }) ↦
            ({ toFun := fun (z : QuadraticAlgebra R a b) ↦ HSMul.hSMul (β := A) z.re 1 + z.im • (↑u : A), map_one' := sorry,
                map_mul' := sorry, map_zero' := sorry, map_add' := sorry, commutes' := sorry } :
              QuadraticAlgebra R a b →ₐ[R] A))
          ((fun (f : QuadraticAlgebra R a b →ₐ[R] A) ↦
              (Subtype.mk (p := fun (u : A) ↦ u * u = HSMul.hSMul (β := A) a 1 + b • u)
                  ((f : (a : QuadraticAlgebra R a b) → A) ω) sorry :
                { u : A // u * u = HSMul.hSMul (β := A) a 1 + b • u }))
            f) :
        (a : QuadraticAlgebra R a b) → A)
      ω :
    A)
  ((f : (a : QuadraticAlgebra R a b) → A) ω : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x y : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
      (star { re := x, im := y : QuadraticAlgebra R a b }) =
    HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
      HMul.hMul (β := QuadraticAlgebra R a b)
        (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)
have re : (HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
      (star { re := x, im := y : QuadraticAlgebra R a b })).re =
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
      HMul.hMul (β := QuadraticAlgebra R a b)
        (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
        (star { re := x, im := y : QuadraticAlgebra R a b })).re =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
          HMul.hMul (β := QuadraticAlgebra R a b)
            (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)).re
have re : x * (x + b * y) + -(a * y * y) = x * x + b * x * y - a * y * y
Tactic: simp