awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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) ↔
    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:
simp [← algebraMap_inj (R := R) (a := a) (b := b)]

Premises used: QuadraticAlgebra.algebraMap_inj
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
⊢ Eq (α := Submonoid (QuadraticAlgebra R a b)) (MonoidHom.mker (F := QuadraticAlgebra R a b →* R) norm)
    (unitary (QuadraticAlgebra R a b))

Tactic:
Submonoid.ext fun _ => norm_eq_one_iff_mem_unitary

Premises used: QuadraticAlgebra.norm_eq_one_iff_mem_unitary, Submonoid.ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
r : R
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
⊢ 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

Tactic:
simp only [mem_nonZeroDivisors_iff_right]

Premises used: mem_nonZeroDivisors_iff_right
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
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
⊢ (∀ (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
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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 : QuadraticAlgebra R a b)
    (0 : QuadraticAlgebra R a b)
rw rw₁ : R
⊢ x = 0

Tactic:
rw [← algebraMap_inj, map_zero]

Premises used: QuadraticAlgebra.algebraMap_inj, map_zero
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
mp₂ mp₃ : Eq.{u_2 + 1} (α := 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

Tactic:
rw [← map_mul, hxr, map_zero]

Premises used: map_zero, map_mul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
⊢ (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

Premises used: QuadraticAlgebra.re_zero, QuadraticAlgebra.im_zero, QuadraticAlgebra.ext_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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.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

Premises used: QuadraticAlgebra.algebraMap_re, zero_add, MulZeroClass.mul_zero, QuadraticAlgebra.im_mul, add_zero, QuadraticAlgebra.re_mul, QuadraticAlgebra.algebraMap_im
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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 : z.re * r = 0 ∧ z.im * r = 0
⊢ z = 0

Tactic:
simp [QuadraticAlgebra.ext_iff, re_zero, im_zero, h _ hz.left, h _ hz.right]

Premises used: QuadraticAlgebra.re_zero, And.right, And.left, QuadraticAlgebra.im_zero, QuadraticAlgebra.ext_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
rw : ∀ (hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0) (x : QuadraticAlgebra R a b), x * star z = 0 → x = 0
⊢ Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star z)

Tactic:
rw [mem_nonZeroDivisors_iff_right] at hz ⊢

Premises used: mem_nonZeroDivisors_iff_right
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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 0
⊢ w = 0

Tactic:
apply star_involutive.injective

Premises used: InvolutiveStar.star_involutive, Function.Involutive.injective
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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 = 0
⊢ star w = star 0

Tactic:
rw [star_zero]

Premises used: star_zero
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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 * z = 0
⊢ star w = 0

Tactic:
apply hz
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
a₅ a₆ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 0 0
⊢ star w * z = 0

Tactic:
rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]

Premises used: InvolutiveStar.star_involutive, star_zero, mul_comm, StarMul.star_mul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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

Tactic:
⟨fun h ↦ ?_, star_mem_nonZeroDivisors⟩

Premises used: QuadraticAlgebra.star_mem_nonZeroDivisors, Iff.intro
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
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
⊢ 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⟩
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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)
rw : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (star (star z))
⊢ Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z

Tactic:
rw [← star_involutive z]

Premises used: InvolutiveStar.star_involutive
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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)⁰ (star (star z))

Tactic:
star_mem_nonZeroDivisors h

Premises used: Set.Mem, QuadraticAlgebra.star_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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)⁰ (star (star z))

Tactic:
exact star_mem_nonZeroDivisors h

Premises used: QuadraticAlgebra.star_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
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
mpr :
  Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ z →
    Membership.mem (α := R) (γ := Submonoid R) R⁰ ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
⊢ 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
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
mp :
  (∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0) →
    ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
⊢ 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:
simp only [mem_nonZeroDivisors_iff_right]

Premises used: mem_nonZeroDivisors_iff_right
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
rw :
  HMul.hMul (α := QuadraticAlgebra R a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra R a b) → R) z) : QuadraticAlgebra R a b) w =
    0
rw₁ :
  HMul.hMul (α := 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)
      w =
    0
rw₂ : z * star z * w = 0
rw₃ : w * (z * star z) = 0
rw₄ : w * z * star z = 0
rw₅ : 0 * star z = 0
rw₆ rw₇ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 0 0
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0

Tactic:
rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_mul]

Premises used: QuadraticAlgebra.C_eq_algebraMap, MulZeroClass.zero_mul, mul_assoc, QuadraticAlgebra.C_mul_eq_smul, mul_comm, QuadraticAlgebra.algebraMap_norm_eq_mul_star
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0

Tactic:
have : norm z • w = 0 := by
      rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_mul]
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
⊢ HMul.hMul (β := R) w.re ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 ∧
    HMul.hMul (β := R) w.im ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0

Tactic:
simp only [QuadraticAlgebra.ext_iff, re_smul, smul_eq_mul, mul_comm, re_zero, im_smul,
      im_zero] at this

Premises used: QuadraticAlgebra.re_zero, QuadraticAlgebra.im_smul, QuadraticAlgebra.re_smul, QuadraticAlgebra.im_zero, mul_comm, smul_eq_mul, QuadraticAlgebra.ext_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this :
  HMul.hMul (β := R) w.re ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 ∧
    HMul.hMul (β := R) w.im ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0
mp : w.re = re (a := a) (b := b) 0
mp₁ : w.im = im (a := a) (b := b) 0
⊢ w = 0

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this :
  HMul.hMul (β := R) w.re ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 ∧
    HMul.hMul (β := R) w.im ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0
⊢ w.re = re (a := a) (b := b) 0

Tactic:
simp [h _ this.left, h _ this.right]

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
R : Type u_2
a b : R
inst : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), HMul.hMul (β := R) x ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this :
  HMul.hMul (β := R) w.re ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0 ∧
    HMul.hMul (β := R) w.im ((norm : (a : QuadraticAlgebra R a b) → R) z : R) = 0
⊢ w.im = im (a := a) (b := b) 0

Tactic:
simp [h _ this.left, h _ this.right]

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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
mpr : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (z * star z)
⊢ Membership.mem (α := R) (γ := Submonoid R) R⁰ ((norm : (a : QuadraticAlgebra R a b) → R) z : R)

Tactic:
rw [← algebraMap_mem_nonZeroDivisors_iff, algebraMap_norm_eq_mul_star]

Premises used: QuadraticAlgebra.algebraMap_norm_eq_mul_star, QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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)⁰ (z * star z)

Tactic:
Submonoid.mul_mem _ hz (star_mem_nonZeroDivisors hz)

Premises used: Submonoid.mul_mem, Set.Mem, QuadraticAlgebra.star_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
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)⁰ (z * star z)

Tactic:
exact Submonoid.mul_mem _ hz (star_mem_nonZeroDivisors hz)

Premises used: Submonoid.mul_mem, QuadraticAlgebra.star_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
mp : Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K) → z = 0
mpr : z = 0 → Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
⊢ Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K) ↔ z = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
⊢ z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0

Tactic:
rw [norm_def] at hz

Premises used: QuadraticAlgebra.norm_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
pos : ∀ (h : z.im = 0), z = 0
neg : ∀ (h : ¬z.im = 0), z = 0
⊢ z = 0

Tactic:
by_cases h : z.im = 0

Premises used: QuadraticAlgebra.im
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : z.im = 0
⊢ z.re = 0

Tactic:
simp [h] at hz
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
h : z.im = 0
hz : z.re = 0
⊢ z = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : ¬z.im = 0
neg : False
⊢ z = 0

Tactic:
exfalso
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : ¬z.im = 0
⊢ HPow.hPow (β := ℕ) z.re 2 = a * z.im * z.im - b * z.re * z.im

Tactic:
rw [← pow_two, sub_eq_zero, ← eq_sub_iff_add_eq] at hz

Premises used: pow_two, sub_eq_zero, eq_sub_iff_add_eq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : ¬z.im = 0
hz₁ : HPow.hPow (β := ℕ) z.re 2 = a * z.im * z.im - b * z.re * z.im
⊢ ¬z.im = 0

Tactic:
rw [← pow_two, sub_eq_zero, ← eq_sub_iff_add_eq] at hz

Premises used: pow_two, sub_eq_zero, eq_sub_iff_add_eq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : HPow.hPow (β := ℕ) z.re 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
neg : HPow.hPow (β := ℕ) (-z.re / z.im) 2 = a + b * (-z.re / z.im)
⊢ False

Tactic:
apply Hab.out (-z.re / z.im)

Premises used: QuadraticAlgebra.re, HDiv.hDiv, QuadraticAlgebra.im, Neg.neg, Fact.out
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : HPow.hPow (β := ℕ) z.re 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
⊢ HPow.hPow (β := ℕ) (-z.re / z.im) 2 = a + b * (-z.re / z.im)

Tactic:
grind
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z = 0
⊢ Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)

Tactic:
simp [hz]
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z ≠ 0
⊢ ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)

Tactic:
rw [ne_eq, ← norm_eq_zero_iff_eq_zero] at hz

Premises used: ne_eq, QuadraticAlgebra.norm_eq_zero_iff_eq_zero
-- Module: Mathlib.Algebra.QuadraticAlgebra.Basic
Goal:
K : Type u_1
R : Type u_2
a_1 b_1 : R
inst : Field K
a b : K
Hab : Fact (∀ (r : K), HPow.hPow (β := ℕ) r 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
simp : HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
⊢ z * z⁻¹ = 1

Tactic:
simp only [inv_def, Algebra.mul_smul_comm]

Premises used: Algebra.mul_smul_comm, QuadraticAlgebra.inv_def