awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 })).im =
    (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)).im
have im : -(x * y) + y * (x + b * y) + -(b * y * y) = 0
Tactic: 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 : CommRing R
a b : QuadraticAlgebra R a_1 b_1
⊢ star (a * b) = star b * star a
have re : (star (a * b)).re = (star b * star a).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 : CommRing R
a b : QuadraticAlgebra R a_1 b_1
re : (star (a * b)).re = (star b * star a).re
⊢ star (a * b) = star b * star a
have im : (star (a * b)).im = (star b * star a).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 : CommRing R
a b : QuadraticAlgebra R a_1 b_1
⊢ (star (a * b)).re = (star b * star a).re
have re : a.re * b.re + a_1 * a.im * b.im + b_1 * (a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
  (b.re + b_1 * b.im) * (a.re + b_1 * a.im) + a_1 * b.im * a.im
Tactic: simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]
-- 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 : CommRing R
a b : QuadraticAlgebra R a_1 b_1
⊢ (star (a * b)).im = (star b * star a).im
have im : -(a.re * b.im + a.im * b.re + b_1 * a.im * b.im) =
  -((b.re + b_1 * b.im) * a.im) + -(b.im * (a.re + b_1 * a.im)) + b_1 * b.im * a.im
Tactic: simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
x x_1 : QuadraticAlgebra R a b
⊢ (star (x + x_1)).re = (star x + star x_1).re
have simp : x.re + x_1.re + b * (x.im + x_1.im) = x.re + b * x.im + (x_1.re + b * x_1.im)
Tactic: simp only [re_star, re_add, im_add]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
a b : R
inst : CommRing R
z w : QuadraticAlgebra R a b
⊢ (z * w).re * (z * w).re + b * (z * w).re * (z * w).im - a * (z * w).im * (z * w).im =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)
have simp : (z.re * w.re + a * z.im * w.im) * (z.re * w.re + a * z.im * w.im) +
      b * (z.re * w.re + a * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) -
    a * (z.re * w.im + z.im * w.re + b * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) =
  (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)
Tactic: simp only [re_mul, im_mul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
      ((norm : (a : QuadraticAlgebra R a b) → R) z) =
    z * star z
have re : re (a := a) (b := b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
      ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
  (z * star z).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
re :
  QuadraticAlgebra.re (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).re
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
      ((norm : (a : QuadraticAlgebra R a b) → R) z) =
    z * star z
have im : im (a := a) (b := b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
      ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
  (z * star z).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ re (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).re
have re : z.re * z.re + z.im * (b * z.re) - z.im * (a * z.im) = z.re * (z.re + b * z.im) + -(z.im * (a * z.im))
Tactic: simp [norm, star, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ im (a := a) (b := b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z)) =
    (z * star z).im
have im : 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))
Tactic: simp [norm, star, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) (star x) : R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
have simp : (x.re + b * x.im) * (x.re + b * x.im) + -(b * (x.re + b * x.im) * x.im) = x.re * x.re + b * x.re * x.im
Tactic: simp only [norm, MonoidHom.coe_mk, OneHom.coe_mk, re_star, im_star, mul_neg, neg_mul, neg_neg,
    sub_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit x ↔ IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
have mp : IsUnit x → IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
mp : IsUnit x → IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
⊢ IsUnit x ↔ IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R)
have mpr : IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) → IsUnit x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit (M := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) → IsUnit x
have mpr : (∃ (b_1 : R),
    HMul.hMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) b_1 = 1 ∧
      HMul.hMul (β := R) b_1 ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1) →
  ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1
Tactic: simp only [isUnit_iff_exists]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : HMul.hMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) x : R) r = 1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
⊢ ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1
have hr₁ : x *
    HMul.hMul (β := QuadraticAlgebra R a b) (star x)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
  1
Tactic: rw [← C_inj (R := R) (a := a) (b := b), C_mul, C_eq_algebraMap, algebraMap_norm_eq_mul_star,
      mul_assoc, map_one] at hr
Cleared hypotheses: hr, hr'
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
⊢ ∃ (b_1 : QuadraticAlgebra R a b), x * b_1 = 1 ∧ b_1 * x = 1
have mpr : HMul.hMul (β := QuadraticAlgebra R a b) (star x)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) *
    x =
  1
Tactic: refine ⟨_, hr, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
hr' : HMul.hMul (β := R) r ((norm : (a : QuadraticAlgebra R a b) → R) x : R) = 1
mpr :
  x *
      HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    1
⊢ HMul.hMul (β := QuadraticAlgebra R a b) (star x)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) *
      x =
    1
have mpr₁ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 1 1
Tactic: rw [mul_comm, hr]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) (1 : R) ↔
    Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (unitary (QuadraticAlgebra R a b)) z
have rw : Eq (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) (1 : R) ↔
  Eq (α := QuadraticAlgebra R a b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b)
        ((norm : (a : QuadraticAlgebra R a b) → R) z) :
      QuadraticAlgebra R a b)
    (1 : QuadraticAlgebra R a b)
Tactic: rw [Unitary.mem_iff_self_mul_star, ← algebraMap_norm_eq_mul_star]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
⊢ Membership.mem (α := QuadraticAlgebra R a b) (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) ↔
    Membership.mem (γ := Submonoid R) R⁰ r
have simp : (∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0) ↔
  ∀ (x : R), x * r = 0 → x = 0
Tactic: simp only [mem_nonZeroDivisors_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
⊢ (∀ (x : QuadraticAlgebra R a b),
      HMul.hMul (β := QuadraticAlgebra R a b) x
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
          0 →
        x = 0) ↔
    ∀ (x : R), x * r = 0 → x = 0
have mp : (∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0) →
  ∀ (x : R), x * r = 0 → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
mp :
  (∀ (x : QuadraticAlgebra R a b),
      HMul.hMul (β := QuadraticAlgebra R a b) x
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
          0 →
        x = 0) →
    ∀ (x : R), x * r = 0 → x = 0
⊢ (∀ (x : QuadraticAlgebra R a b),
      HMul.hMul (β := QuadraticAlgebra R a b) x
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
          0 →
        x = 0) ↔
    ∀ (x : R), x * r = 0 → x = 0
have mpr : (∀ (x : R), x * r = 0 → x = 0) →
  ∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_2 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
H :
  ∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0
x : R
hxr : x * r = 0
⊢ x = 0
have mp : Eq (α := QuadraticAlgebra R a b)
  ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
  (0 : QuadraticAlgebra R a b)
Tactic: rw [← algebraMap_inj, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
H :
  ∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0
x : R
hxr : x * r = 0
⊢ 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) r : QuadraticAlgebra R a b) =
    0
have mp : Eq (α := QuadraticAlgebra R a b)
  ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) (x * r) : QuadraticAlgebra R a b)
  (0 : QuadraticAlgebra R a b)
Tactic: rw [← map_mul, hxr, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
H :
  ∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0
x : R
hxr : x * r = 0
mp :
  Eq (α := QuadraticAlgebra R a b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) (x * r) : QuadraticAlgebra R a b)
    (0 : 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) r : QuadraticAlgebra R a b) =
    0
have mp₁ : Eq (α := QuadraticAlgebra R a b) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) 0) 0
Tactic: rw [← map_mul, hxr, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
H :
  ∀ (x : QuadraticAlgebra R a b),
    HMul.hMul (β := QuadraticAlgebra R a b) x
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
        0 →
      x = 0
x : R
hxr : x * r = 0
mp :
  Eq (α := QuadraticAlgebra R a b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) (x * r) : QuadraticAlgebra R a b)
    (0 : QuadraticAlgebra R a b)
mp₁ :
  Eq (α := QuadraticAlgebra R a b) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) 0) 0
⊢ 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) r : QuadraticAlgebra R a b) =
    0
have mp₂ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 0 0
Tactic: rw [← map_mul, hxr, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz :
  HMul.hMul (β := QuadraticAlgebra R a b) z
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b) =
    0
⊢ z = 0
have hz₁ : (HMul.hMul (β := QuadraticAlgebra R a b) z
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b)).re =
    0 ∧
  (HMul.hMul (β := QuadraticAlgebra R a b) z
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b)).im =
    0
Tactic: rw [QuadraticAlgebra.ext_iff, re_zero, im_zero] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz :
  (HMul.hMul (β := QuadraticAlgebra R a b) z
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r :
            QuadraticAlgebra R a b)).re =
      0 ∧
    (HMul.hMul (β := QuadraticAlgebra R a b) z
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r :
            QuadraticAlgebra R a b)).im =
      0
⊢ z = 0
have hz₁ : z.re * r = 0 ∧ z.im * r = 0
Tactic: simp only [re_mul, algebraMap_re, algebraMap_im, mul_zero, add_zero, im_mul, zero_add] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
⊢ Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star z)
have rw : ∀ (hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0) (x : QuadraticAlgebra R a b), x * star z = 0 → x = 0
Tactic: rw [mem_nonZeroDivisors_iff_right] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ w = 0
have a₁ : star w = star 0
Tactic: apply star_involutive.injective
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star w = star 0
have a₁ : star w = 0
Tactic: rw [star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star w = 0
have a₁ : star w * z = 0
Tactic: apply hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star w * z = 0
have a₁ : star w * star (star z) = 0
Tactic: rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
a₁ : star w * star (star z) = 0
⊢ star w * z = 0
have a₂ : star (star z * w) = 0
Tactic: rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
a₁ : star w * star (star z) = 0
a₂ : star (star z * w) = 0
⊢ star w * z = 0
have a₃ : star (w * star z) = 0
Tactic: rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
a₁ : star w * star (star z) = 0
a₂ : star (star z * w) = 0
a₃ : star (w * star z) = 0
⊢ star w * z = 0
have a₄ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) (star 0) 0
Tactic: rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
a₁ : star w * star (star z) = 0
a₂ : star (star z * w) = 0
a₃ : star (w * star z) = 0
a₄ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) (star 0) 0
⊢ star w * z = 0
have a₅ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 0 0
Tactic: rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star z) ↔
    Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
have refine : ∀ (h : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star z)),
  Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
Tactic: refine ⟨fun h ↦ ?_, star_mem_nonZeroDivisors⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star z)
⊢ Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
have rw : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star (star z))
Tactic: rw [← star_involutive z]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
⊢ Membership.mem (α := R) (γ := Submonoid R) R⁰ ((norm : (a : QuadraticAlgebra R a b) → R) z : R) ↔
    Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
have mp : Membership.mem (α := R) (γ := Submonoid R) R⁰ ((norm : (a : QuadraticAlgebra R a b) → R) z : R) →
  Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z
Tactic: constructor