awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * HMul.hMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) *
      (s * HMul.hMul (β := R) s ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) =
    s * HMul.hMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) *
      (r * HMul.hMul (β := R) s ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have this₁ : r * r * s * s *
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
  r * r * s * s *
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have hrs : r * r * s * s ≠ 0
Tactic: have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have neg : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)
    ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (s • y) : R) =
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (s • y) : R)
    ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)
Tactic: suffices
        (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
      simp only [map_smul, smul_apply, smul_eq_mul] at this
      rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
      have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
      exact le_of_eq <| mul_right_injective₀ hrs this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
⊢ s • y = -r • x
have rwa : s • y = -(r • x)
Tactic: rwa [neg_smul, ← add_eq_zero_iff_eq_neg']
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ LinearIndependent R ![x, y] →
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
have mpr : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) →
  ¬LinearIndependent R ![x, y]
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw₁ : HMul.hMul (α := R) (β := R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R) =
  HMul.hMul (α := R) (β := R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R) =
    HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) =
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    LinearIndependent R ![x, y]
have rw : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
  LinearIndependent R ![x, y]
Tactic: rw [show B x y ^ 2 = B x y * B y x by rw [sq, ← hB.eq, RingHom.id_apply]]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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
⊢ (∀ (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)) →
    B.IsSymm
have refine : ∀
  (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),
  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: refine fun h ↦ ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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
⊢ 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)
have obtain : ∀ (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),
  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 ⟨fx, tx, ix, -, hx⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : x ∈ Submodule.span R (Set.range b))
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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 (α := 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)
have 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)
Tactic: rw [← hx, ← hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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 (α := 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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)
    (∑ 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))
have 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))
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
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
⊢ 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)
have 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)
Tactic: rw [mul_left_comm]