awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      z =
    HMul.hMul (β := QuadraticAlgebra R a b) z
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
have re : (HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      z).re =
  (HMul.hMul (β := QuadraticAlgebra R a b) z
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
z : QuadraticAlgebra R a b
re :
  (HMul.hMul (α := QuadraticAlgebra R a b)
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)
        z).re =
    (HMul.hMul (β := QuadraticAlgebra R a b) z
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)).re
⊢ HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      z =
    HMul.hMul (β := QuadraticAlgebra R a b) z
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
have im : (HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      z).im =
  (HMul.hMul (β := QuadraticAlgebra R a b) z
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ s • x =
    HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      x
have re : (s • x).re =
  (HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x_1 y : QuadraticAlgebra R a b
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
x : QuadraticAlgebra R a b
re :
  (s • x).re =
    (HMul.hMul (α := QuadraticAlgebra R a b)
        (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
              (a_1 : S) → QuadraticAlgebra R a b)
            s :
          QuadraticAlgebra R a b)
        x).re
⊢ s • x =
    HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      x
have im : (s • x).im =
  (HMul.hMul (α := QuadraticAlgebra R a b)
      (({ toFun := fun (s : S) ↦ QuadraticAlgebra.C ((algebraMap S R : (a : S) → R) s), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_2, u_1} S (QuadraticAlgebra R a b) } :
            (a_1 : S) → QuadraticAlgebra R a b)
          s :
        QuadraticAlgebra R a b)
      x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ x * QuadraticAlgebra.C r = r • x
have rw : QuadraticAlgebra.C r * x = r • x
Tactic: rw [mul_comm, C_mul_eq_smul r x]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
x : QuadraticAlgebra R a b
rw : QuadraticAlgebra.C r * x = r • x
⊢ x * QuadraticAlgebra.C r = r • x
have rw₁ : r • x = r • x
Tactic: rw [mul_comm, C_mul_eq_smul r x]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r1 r2 : R
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) = QuadraticAlgebra.C (r1 * r2)
have rw : HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) =
  HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r1) (QuadraticAlgebra.C r2)
Tactic: rw [C_mul, C_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r1 r2 : R
rw :
  HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) =
    HMul.hMul (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r1) (QuadraticAlgebra.C r2)
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) = QuadraticAlgebra.C (r1 * r2)
have rw₁ : HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) =
  HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2)
Tactic: rw [C_mul, C_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im
have mp : (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r ∣ z → r ∣ z.re ∧ r ∣ z.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
z : QuadraticAlgebra R a b
mp : (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r ∣ z → r ∣ z.re ∧ r ∣ z.im
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im
have mpr : r ∣ z.re ∧ r ∣ z.im → (algebraMap R (QuadraticAlgebra R a b) : (a_2 : R) → QuadraticAlgebra R a b) r ∣ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r_1 : R
z : QuadraticAlgebra R a b
r : R
hr : z.re = r_1 * r
i : R
hi : z.im = r_1 * i
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r_1 ∣ z
have h : z =
  HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r_1 : QuadraticAlgebra R a b)
    ({ re := r, im := i } : QuadraticAlgebra R a b)
Tactic: use ⟨r, i⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
z w : R
⊢ Dvd.dvd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) z : QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) w : QuadraticAlgebra R a b) ↔
    z ∣ w
have rw : z ∣ re (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) w) ∧
    z ∣ im (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) w) ↔
  z ∣ w
Tactic: rw [algebraMap_dvd_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommRing R
n : ℤ
x y : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b } =
    { re := (↑n : R) * x, im := (↑n : R) * y }
have re : (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
      { re := x, im := y : QuadraticAlgebra R a b }).re =
  re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Defs (goal)
Goal:
R : Type u_1
a b : R
inst : CommRing R
n : ℤ
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b } =
    { re := (↑n : R) * x, im := (↑n : R) * y }
have im : (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
      { re := x, im := y : QuadraticAlgebra R a b }).im =
  im (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ Eq (α := R)
    (((LinearMap.det.{u_1, u_1} (M := QuadraticAlgebra R a b) (A := R) :
            (QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) →* R) :
          (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → R)
        (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) :
      R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
have rw : Eq (α := R)
  (Matrix.det (n := Fin 2)
      ((LinearMap.toMatrix (basis a b) (basis a b) :
          (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → Matrix (Fin 2) (Fin 2) R)
        (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)) :
    R)
  ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
Tactic: rw [← LinearMap.det_toMatrix <| basis ..]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
have simp : z.re * (z.re + b * z.im) = z.re * z.re + b * z.re * z.im
Tactic: simp [norm]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ Eq (α := R)
    (Matrix.det (n := Fin 2)
        ((LinearMap.toMatrix (basis a b) (basis a b) :
            (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → Matrix (Fin 2) (Fin 2) R)
          (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)) :
      R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
have this : Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
  ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
Tactic: have : !![z.re, a * z.im; z.im, z.re + b * z.im].det = z.norm := by
    simp [norm]
    ring
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
⊢ Eq (α := R)
    (Matrix.det (n := Fin 2)
        ((LinearMap.toMatrix (basis a b) (basis a b) :
            (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → Matrix (Fin 2) (Fin 2) R)
          (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)) :
      R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
have h : Eq (α := Matrix (Fin 2) (Fin 2) R)
  ((LinearMap.toMatrix (basis a b) (basis a b) :
        (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → Matrix (Fin 2) (Fin 2) R)
      (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) :
    Matrix (Fin 2) (Fin 2) R)
  (!![z.re, a * z.im; z.im, z.re + b * z.im] : Matrix (Fin 2) (Fin 2) R)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) R)
    ((LinearMap.toMatrix (basis a b) (basis a b) :
          (a : QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) → Matrix (Fin 2) (Fin 2) R)
        (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) :
      Matrix (Fin 2) (Fin 2) R)
    (!![z.re, a * z.im; z.im, z.re + b * z.im] : Matrix (Fin 2) (Fin 2) R)
have h : Eq (α := QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)
  ((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
      (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
    !![z.re, a * z.im; z.im, z.re + b * z.im])
Tactic: apply LinearEquiv.eq_symm_apply _ |>.mp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
⊢ Eq (α := QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)
    ((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
        (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
      !![z.re, a * z.im; z.im, z.re + b * z.im])
have h : ∀ (w : QuadraticAlgebra R a b),
  Eq (α := QuadraticAlgebra R a b)
    ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z : (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w :
      QuadraticAlgebra R a b)
    ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
              !![z.re, a * z.im; z.im, z.re + b * z.im] :
            QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
          (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w :
      QuadraticAlgebra R a b)
Tactic: ext1 w
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := QuadraticAlgebra R a b)
    ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z : (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w :
      QuadraticAlgebra R a b)
    ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
              !![z.re, a * z.im; z.im, z.re + b * z.im] :
            QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
          (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w :
      QuadraticAlgebra R a b)
have h : Eq (α := Fin 2 →₀ R)
  ((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
      ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z : (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w) :
    Fin 2 →₀ R)
  ((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
      ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
              !![z.re, a * z.im; z.im, z.re + b * z.im] :
            QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
          (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
        w) :
    Fin 2 →₀ R)
Tactic: apply basis .. |>.repr.injective
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := Fin 2 →₀ R)
    ((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
        ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
            (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
          w) :
      Fin 2 →₀ R)
    ((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
        ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                  (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
                !![z.re, a * z.im; z.im, z.re + b * z.im] :
              QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
            (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
          w) :
      Fin 2 →₀ R)
have h : Eq (α := (a : Fin 2) → R)
  (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
          ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
              (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
            w) :
        Fin 2 →₀ R) :
    (a : Fin 2) → R)
  (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
          ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                    (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
                  !![z.re, a * z.im; z.im, z.re + b * z.im] :
                QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
              (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
            w) :
        Fin 2 →₀ R) :
    (a : Fin 2) → R)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := (a : Fin 2) → R)
    (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
      (a : Fin 2) → R)
    (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                      (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
                    !![z.re, a * z.im; z.im, z.re + b * z.im] :
                  QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
      (a : Fin 2) → R)
have h : Eq (α := (a : Fin 2) → R)
  (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
          ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
              (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
            w) :
        Fin 2 →₀ R) :
    (a : Fin 2) → R)
  (Matrix.mulVec (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
    (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R))
Tactic: rw [LinearMap.toMatrix_symm, Matrix.repr_toLin]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := (a : Fin 2) → R)
    (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
      (a : Fin 2) → R)
    (Matrix.mulVec (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R))
have h : ∀ (i : Fin 2),
  Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        i :
      R)
    (Matrix.mulVec (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R)
      i)
Tactic: ext i