-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
rw :
  LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (range (v ∘ Sum.inr)))
rw₁ rw₂ rw₃ :
  LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
refine_1 :
  LinearIndependent R v →
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
refine_2 refine_2₁ :
  LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)) →
    LinearIndependent R v
refine_2₂ :
  ∀ (hl : LinearIndependent R (v ∘ Sum.inl)) (hr : LinearIndependent R (v ∘ Sum.inr))
    (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))),
    LinearIndependent R v
refine_2₃ refine_2₄ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)))
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι')
    (hi : i ∈ s), g i = 0
refine_2₅ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)))
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι') (hi : i ∈ s)
    (this :
      HAdd.hAdd (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
          (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) =
        0),
    g i = 0
refine_2₆ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)))
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι') (hi : i ∈ s)
    (this :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
        (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))),
    g i = 0
refine_2₇ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr :
      ∀ (x : M),
        Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
          ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0)
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι') (hi : i ∈ s)
    (this :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
        (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))),
    g i = 0
refine_2₈ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr :
      ∀ (x : M),
        Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
          ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0)
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι') (hi : i ∈ s)
    (this :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
        (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)))
    (A : Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0), g i = 0
refine_2₉ :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr :
      ∀ (x : M),
        Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
          ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0)
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0)
    (this :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
        (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)))
    (A : Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0) (i : ι)
    (hi : Sum.inl i ∈ s), g (Sum.inl i) = 0
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))
have refine_2₁₀ : ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
  (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
  (hlr :
    ∀ (x : M),
      Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
        ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0)
  (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0)
  (this :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl sorry, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
      (-∑ i ∈ s.preimage Sum.inr sorry, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)))
  (A : Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl sorry, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0) (i : ι')
  (hi : Sum.inr i ∈ s), g (Sum.inr i) = 0
Tactic: classical
  rw [range_comp v, range_comp v]
  refine ⟨?_, ?_⟩
  · intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint
  rintro ⟨hl, hr, hlr⟩
  rw [linearIndependent_iff'] at *
  intro s g hg i hi
  have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 := by
    -- Porting note: `g` must be specified.
    rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
    · exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
  rw [← eq_neg_iff_add_eq_zero] at this
  rw [disjoint_def'] at hlr
  have A := by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
  rcases i with i | i
  · exact hl _ _ A i (Finset.mem_preimage.2 hi)
  · rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)