awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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).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

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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).im =
    (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)).im

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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
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' := ⋯, 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).im
⊢ 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

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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).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

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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).im =
    (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).im

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
⊢ Eq (α := QuadraticAlgebra R a b)
    ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b)
    ({ re := r, im := 0 } : QuadraticAlgebra R a b)

Tactic:
rfl

Premises used: QuadraticAlgebra.C, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
x x_1 : R
⊢ Eq (α := 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_1 : QuadraticAlgebra R a b) →
    x = x_1

Tactic:
simp [algebraMap_eq]

Premises used: QuadraticAlgebra.algebraMap_eq
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
x y : R
⊢ Eq (α := 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) y : QuadraticAlgebra R a b) ↔
    x = y

Tactic:
algebraMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, QuadraticAlgebra.algebraMap_injective
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b r : R
inst : CommSemiring R
⊢ re (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r) = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b r : R
inst : CommSemiring R
⊢ im (a := a) ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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 : Semiring S
inst_2 : Module S R
inst_3 : Module.IsTorsionFree S R
⊢ ∀ (r : S) (m : QuadraticAlgebra R a b),
    (linearEquivTuple a b : (a : QuadraticAlgebra R a b) → Fin 2 → R) (r • m) =
      HSMul.hSMul (β := Fin 2 → R) r ((linearEquivTuple a b : (a : QuadraticAlgebra R a b) → Fin 2 → R) m : Fin 2 → R)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
r : R
⊢ QuadraticAlgebra.C (r ^ n) = HPow.hPow (α := QuadraticAlgebra R a b) (QuadraticAlgebra.C r) n

Tactic:
(algebraMap R (QuadraticAlgebra R a b)).map_pow r n

Premises used: QuadraticAlgebra, Algebra.algebraMap, QuadraticAlgebra.C, RingHom.map_pow
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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
rw₁ rw₂ : r • x = r • x
⊢ x * QuadraticAlgebra.C r = r • x

Tactic:
rw [mul_comm, C_mul_eq_smul r x]

Premises used: QuadraticAlgebra.C_mul_eq_smul, mul_comm
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
⊢ Eq (α := (x : R) → QuadraticAlgebra R a b) QuadraticAlgebra.C
    (⇑(algebraMap R (QuadraticAlgebra R a b)) : (a_1 : R) → QuadraticAlgebra R a b)

Tactic:
rfl

Premises used: QuadraticAlgebra.C, rfl
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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)
rw₁ rw₂ :
  HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) =
    HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2)
⊢ HSMul.hSMul (β := QuadraticAlgebra R a b) r1 (QuadraticAlgebra.C r2) = QuadraticAlgebra.C (r1 * r2)

Tactic:
rw [C_mul, C_mul_eq_smul]

Premises used: QuadraticAlgebra.C_mul, QuadraticAlgebra.C_mul_eq_smul
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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
mpr : r ∣ z.re ∧ r ∣ z.im → (algebraMap R (QuadraticAlgebra R a b) : (a_2 : R) → QuadraticAlgebra R a b) r ∣ z
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im

Tactic:
constructor
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ r ∣
      (HMul.hMul (α := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b)
          x).re ∧
    r ∣
      (HMul.hMul (α := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r : QuadraticAlgebra R a b)
          x).im

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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
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)
⊢ (algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) r_1 ∣ z

Tactic:
use ⟨r, i⟩
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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
⊢ 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:
simp [QuadraticAlgebra.ext_iff, hr, hi, ← C_eq_algebraMap]

Premises used: QuadraticAlgebra.C_eq_algebraMap, QuadraticAlgebra.ext_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
z w : R
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
⊢ 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

Tactic:
rw [algebraMap_dvd_iff]

Premises used: QuadraticAlgebra.algebraMap_dvd_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
z w : R
⊢ 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:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst : CommRing R
inst_1 : CharZero R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := QuadraticAlgebra R a b) (↑m : QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b) → m = n

Tactic:
simp [QuadraticAlgebra.ext_iff]

Premises used: QuadraticAlgebra.ext_iff
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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 }
im :
  (HMul.hMul (α := QuadraticAlgebra R a b) (↑n : QuadraticAlgebra R a b)
        { re := x, im := y : QuadraticAlgebra R a b }).im =
    QuadraticAlgebra.im (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 }

Tactic:
ext
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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 =
    re (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.Defs
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 }).im =
    im (a := a) (b := b) { re := (↑n : R) * x, im := (↑n : R) * y }

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
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)
⊢ 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)

Tactic:
rw [← LinearMap.det_toMatrix <| basis ..]

Premises used: QuadraticAlgebra.basis, LinearMap.det_toMatrix
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
simp : z.re * (z.re + b * z.im) = z.re * z.re + b * z.re * z.im
⊢ 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:
simp [norm]

Premises used: QuadraticAlgebra.norm
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ z.re * (z.re + b * z.im) = z.re * z.re + b * z.re * z.im

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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)

Tactic:
have : !![z.re, a * z.im; z.im, z.re + b * z.im].det = z.norm := by
    simp [norm]
    ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)

Tactic:
this
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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)
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)
⊢ 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:
convert! this
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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)
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])
⊢ 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:
apply LinearEquiv.eq_symm_apply _ |>.mp

Premises used: LinearEquiv.eq_symm_apply, Iff.mp
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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)
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)
⊢ 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:
ext1 w
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
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)
⊢ 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:
apply basis .. |>.repr.injective

Premises used: Module.Basis.repr, QuadraticAlgebra.basis, LinearEquiv.injective
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
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)
⊢ 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 DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'