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
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
⊢ 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 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)
Tactic: constructor
-- 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 : (∀ (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
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
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
have rw : HMul.hMul (α := QuadraticAlgebra R a b)
    (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra R a b) → R) z) : QuadraticAlgebra R a b) w =
  0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have 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
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have rw₂ : z * star z * w = 0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have rw₃ : w * (z * star z) = 0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have rw₄ : w * z * star z = 0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have rw₅ : 0 * star z = 0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_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
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
⊢ HSMul.hSMul (α := R) ((norm : (a : QuadraticAlgebra R a b) → R) z : R) w = 0
have rw₆ : Eq.{u_2 + 1} (α := QuadraticAlgebra R a b) 0 0
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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
⊢ w = 0
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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
⊢ w = 0
have 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
Tactic: simp only [QuadraticAlgebra.ext_iff, re_smul, smul_eq_mul, mul_comm, re_zero, im_smul,
      im_zero] at this
Cleared hypotheses: this
-- 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 : ∀ (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 = 0
have mp : w.re = re (a := a) (b := b) 0
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
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
⊢ w = 0
have mp₁ : w.im = im (a := a) (b := b) 0
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
hz : 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)
have mpr : Membership.mem (γ := Submonoid (QuadraticAlgebra R a b)) (QuadraticAlgebra R a b)⁰ (z * star z)
Tactic: rw [← algebraMap_mem_nonZeroDivisors_iff, algebraMap_norm_eq_mul_star]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K) ↔ z = 0
have mp : Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K) → z = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K) ↔ z = 0
have mpr : z = 0 → Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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 = 0
have hz₁ : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
Tactic: rw [norm_def] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ z = 0
have pos : ∀ (h : z.im = 0), z = 0
Tactic: by_cases h : z.im = 0
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ z = 0
have neg : ∀ (h : ¬z.im = 0), z = 0
Tactic: by_cases h : z.im = 0
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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 = 0
have hz₁ : z.re = 0
Tactic: simp [h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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 = 0
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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
⊢ False
have hz₁ : 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
Cleared hypotheses: hz, h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
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
⊢ False
have neg : HPow.hPow (β := ℕ) (-z.re / z.im) 2 = a + b * (-z.re / z.im)
Tactic: apply Hab.out (-z.re / z.im)
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (hypothesis)
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
⊢ z * z⁻¹ = 1
have hz₁ : ¬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
Cleared hypotheses: hz
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
⊢ z * z⁻¹ = 1
have simp : HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
Tactic: simp only [inv_def, Algebra.mul_smul_comm]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw : HMul.hMul (α := QuadraticAlgebra K a b)
    (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
  1
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw₁ : HMul.hMul (α := QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
      QuadraticAlgebra K a b)
    (z * star z) =
  1
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
rw₁ :
  HMul.hMul (α := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      (z * star z) =
    1
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw₂ : HMul.hMul (α := QuadraticAlgebra K a b) (β := QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
      QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        ((norm : (a : QuadraticAlgebra K a b) → K) z) :
      QuadraticAlgebra K a b) =
  1
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
rw₁ :
  HMul.hMul (α := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      (z * star z) =
    1
rw₂ :
  HMul.hMul (α := QuadraticAlgebra K a b) (β := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z) :
        QuadraticAlgebra K a b) =
    1
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw₃ : Eq (α := QuadraticAlgebra K a b)
  ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
      (HMul.hMul (α := K) (β := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K)
        ((norm : (a : QuadraticAlgebra K a b) → K) z : K)) :
    QuadraticAlgebra K a b)
  (1 : QuadraticAlgebra K a b)
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
rw₁ :
  HMul.hMul (α := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      (z * star z) =
    1
rw₂ :
  HMul.hMul (α := QuadraticAlgebra K a b) (β := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z) :
        QuadraticAlgebra K a b) =
    1
rw₃ :
  Eq (α := QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        (HMul.hMul (α := K) (β := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K)
          ((norm : (a : QuadraticAlgebra K a b) → K) z : K)) :
      QuadraticAlgebra K a b)
    (1 : QuadraticAlgebra K a b)
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw₄ : Eq (α := QuadraticAlgebra K a b) ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b) 1) 1
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
z : QuadraticAlgebra K a b
hz : ¬Eq (α := K) ((norm : (a : QuadraticAlgebra K a b) → K) z : K) (0 : K)
rw :
  HMul.hMul (α := QuadraticAlgebra K a b)
      (QuadraticAlgebra.C ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : QuadraticAlgebra K a b) (z * star z) =
    1
rw₁ :
  HMul.hMul (α := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      (z * star z) =
    1
rw₂ :
  HMul.hMul (α := QuadraticAlgebra K a b) (β := QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ :
        QuadraticAlgebra K a b)
      ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
          ((norm : (a : QuadraticAlgebra K a b) → K) z) :
        QuadraticAlgebra K a b) =
    1
rw₃ :
  Eq (α := QuadraticAlgebra K a b)
    ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b)
        (HMul.hMul (α := K) (β := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K)
          ((norm : (a : QuadraticAlgebra K a b) → K) z : K)) :
      QuadraticAlgebra K a b)
    (1 : QuadraticAlgebra K a b)
rw₄ :
  Eq (α := QuadraticAlgebra K a b) ((algebraMap K (QuadraticAlgebra K a b) : (a_2 : K) → QuadraticAlgebra K a b) 1) 1
⊢ HSMul.hSMul (α := K) (((norm : (a : QuadraticAlgebra K a b) → K) z)⁻¹ : K) (z * star z) = 1
have rw₅ : Eq.{u_1 + 1} (α := QuadraticAlgebra K a b) 1 1
Tactic: rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]
-- 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)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra K a b) 0⁻¹ 0
have re : Eq.{u_1 + 1} (α := K) (re (a := a) (b := b) 0⁻¹) (re (a := a) (b := b) 0)
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)
re : Eq.{u_1 + 1} (α := K) (QuadraticAlgebra.re (a := a) (b := b) 0⁻¹) (QuadraticAlgebra.re (a := a) (b := b) 0)
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra K a b) 0⁻¹ 0
have im : Eq.{u_1 + 1} (α := K) (im (a := a) (b := b) 0⁻¹) (im (a := a) (b := b) 0)
Tactic: ext