awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
obtain :
  ∀ (fy : M → R) (ty : Finset M) (iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M))
    (hy : ∑ a ∈ ty, fy a • a = y),
    Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))

Premises used: Submodule.mem_span_iff_exists_finset_subset, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
rw :
  Eq (α := R)
    ((starRingEnd R : (a : R) → R)
        ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ tx, fx a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ ty, fy a • a) : R) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ ty, fy a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ tx, fx a • a) : R)
⊢ Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [← hx, ← hy]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ ty,
      ∑ x_1 ∈ tx,
        star (fy x) *
          HMul.hMul (β := R) (fx x_1) (star ((((B : (a : M) → M →ₗ[R] R) x_1 : M →ₗ[R] R) : (a : M) → R) x) : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty,
        fx x * HMul.hMul (β := R) (star (fy i)) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
⊢ Eq (α := R)
    ((starRingEnd R : (a : R) → R)
        ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ tx, fx a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ ty, fy a • a) : R) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ ty, fy a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ tx, fx a • a) : R)

Tactic:
simp only [map_sum, LinearMap.map_smulₛₗ, starRingEnd_apply, map_smul, coe_sum,
      Finset.sum_apply, smul_apply, smul_eq_mul, Finset.mul_sum, map_mul, star_star]

Premises used: Finset.mul_sum, star_star, LinearMap.smul_apply, Finset.sum_apply, LinearMap.coe_sum, starRingEnd_apply, map_sum, map_mul, LinearMap.map_smulₛₗ, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ y ∈ tx,
      ∑ x ∈ ty,
        star (fy x) *
          HMul.hMul (β := R) (fx y) (star ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x) : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty,
        fx x * HMul.hMul (β := R) (star (fy i)) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ ty,
      ∑ x_1 ∈ tx,
        star (fy x) *
          HMul.hMul (β := R) (fx x_1) (star ((((B : (a : M) → M →ₗ[R] R) x_1 : M →ₗ[R] R) : (a : M) → R) x) : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty,
        fx x * HMul.hMul (β := R) (star (fy i)) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y ∈ tx,
      ∑ x ∈ ty,
        star (fy x) *
          HMul.hMul (β := R) (fx y) (star ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x) : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty,
        fx x * HMul.hMul (β := R) (star (fy i)) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
refine :
  ∀ (b₁ : M) (h₁ : b₁ ∈ tx) (b₂ : M) (h₂ : b₂ ∈ ty),
    star (fy b₂) *
        HMul.hMul (β := R) (fx b₁) (star ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
      fx b₁ * HMul.hMul (β := R) (star (fy b₂)) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y ∈ tx,
      ∑ x ∈ ty,
        star (fy x) *
          HMul.hMul (β := R) (fx y) (star ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x) : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty,
        fx x * HMul.hMul (β := R) (star (fy i)) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
rw :
  fx b₁ * HMul.hMul (β := R) (star (fy b₂)) (star ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx b₁ * HMul.hMul (β := R) (star (fy b₂)) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
⊢ star (fy b₂) * HMul.hMul (β := R) (fx b₁) (star ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx b₁ * HMul.hMul (β := R) (star (fy b₂)) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)

Tactic:
rw [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
obtain :
  ∀ (i : ι) (h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)),
    fx ((b : (a : ι) → M) i) *
        HMul.hMul (β := R) (star (fy b₂))
          (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
      fx ((b : (a : ι) → M) i) *
        HMul.hMul (β := R) (star (fy b₂))
          ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ fx b₁ * HMul.hMul (β := R) (star (fy b₂)) (star ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx b₁ * HMul.hMul (β := R) (star (fy b₂)) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)

Tactic:
obtain ⟨i, rfl⟩ := ix h₁

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₂ : M
h₂ : b₂ ∈ ty
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
obtain :
  ∀ (j : ι) (h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)),
    fx ((b : (a : ι) → M) i) *
        HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
          (star
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) j : M)) :
            R) =
      fx ((b : (a : ι) → M) i) *
        HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)

Tactic:
obtain ⟨j, rfl⟩ := iy h₂

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
j : ι
h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)
rw rw₁ :
  fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
          R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Fintype n
inst_5 : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
rw :
  (∀ (b_1 a : n),
      Eq.{u_1 + 1} (α := R)
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) a) : M →ₗ[R] R) : (a : M) → R)
              ((b : (a : n) → M) b_1 : M)) :
          R)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) b_1) : M →ₗ[R] R) : (a : M) → R) ((b : (a : n) → M) a : M) :
          R)) ↔
    ∀ (i j : n),
      Eq.{u_1 + 1} (α := R) (star ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B j i) : R)
        ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B i j : R)
⊢ B.IsSymm ↔
    Matrix.IsHermitian.{u_1, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)

Tactic:
rw [isSymm_iff_basis b, Matrix.IsHermitian.ext_iff, forall_comm]

Premises used: Matrix.IsHermitian.ext_iff, forall_comm, LinearMap.isSymm_iff_basis
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Fintype n
inst_5 : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (b_1 a : n),
      Eq.{u_1 + 1} (α := R)
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) a) : M →ₗ[R] R) : (a : M) → R)
              ((b : (a : n) → M) b_1 : M)) :
          R)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) b_1) : M →ₗ[R] R) : (a : M) → R) ((b : (a : n) → M) a : M) :
          R)) ↔
    ∀ (i j : n),
      Eq.{u_1 + 1} (α := R) (star ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B j i) : R)
        ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B i j : R)

Tactic:
simp [Eq.comm]

Premises used: Eq.comm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Fintype n
inst_5 : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
x y : n → R
⊢ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) y =
    (((B : (a : M) → M →ₗ[R] R) ((b.equivFun.symm : (a : n → R) → M) x) : M →ₗ[R] R) : (a : M) → R)
      ((b.equivFun.symm : (a : n → R) → M) y : M)

Tactic:
dotProduct_toMatrix₂_mulVec b b B x y

Premises used: dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Fintype n
inst_5 : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    (dotProduct.{u_1, u_3} (m := n) (star (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
        (Matrix.mulVec (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
          (⇑((b.repr : (a : M) → n →₀ R) y : n →₀ R) : (a : n) → R)) :
      R)

Tactic:
apply_eq_dotProduct_toMatrix₂_mulVec b b B x y

Premises used: apply_eq_dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
rw :
  B.IsSymm ∧ B.IsNonneg ↔
    Matrix.IsHermitian.{u_4, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) ∧
      ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
⊢ B.IsPosSemidef ↔
    Matrix.PosSemidef.{u_3, u_4} (n := n) (R := R) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)

Tactic:
rw [isPosSemidef_def, Matrix.posSemidef_iff_dotProduct_mulVec]

Premises used: LinearMap.isPosSemidef_def, Matrix.posSemidef_iff_dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
apply :
  B.IsNonneg ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
⊢ B.IsSymm ∧ B.IsNonneg ↔
    Matrix.IsHermitian.{u_4, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) ∧
      ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x

Tactic:
apply and_congr (B.isSymm_iff_isHermitian_toMatrix b)

Premises used: and_congr, LinearMap.isSymm_iff_isHermitian_toMatrix
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
rw :
  (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
⊢ B.IsNonneg ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x

Tactic:
rw [isNonneg_def]

Premises used: LinearMap.isNonneg_def
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x

Tactic:
⟨fun h x ↦ ?_, fun h x ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
refine_1 :
  ∀ (h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
    (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
refine_2 :
  ∀ (h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x)
    (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x : n → R
refine_1 :
  LE.le.{u_4} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R) ((b.equivFun.symm : (a : n → R) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((b.equivFun.symm : (a : n → R) → M) x : M) :
      R)
⊢ 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x

Tactic:
rw [star_dotProduct_toMatrix₂_mulVec]

Premises used: star_dotProduct_toMatrix₂_mulVec
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x : n → R
⊢ LE.le.{u_4} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R) ((b.equivFun.symm : (a : n → R) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((b.equivFun.symm : (a : n → R) → M) x : M) :
      R)

Tactic:
h _