-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this :
      Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)),
    w i = 0
rw₅ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this :
      Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V))
    (hsum :
      ∑ j ∈ s,
          HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
            ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)),
    w i = 0
rw₆ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (hsum :
      ∑ j ∈ s,
          HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
            ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V))
    (this :
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
        0),
    w i = 0
⊢ LinearIndependent K₁ v
have rw₇ : ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (hsum :
    ∑ j ∈ s,
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V))
  (this :
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      0),
  Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) (w i) : K) (0 : K)
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
    have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
    simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
    apply (map_eq_zero I₁).mp
    exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)