awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
rw :
  Eq.{u_4 + 1} (α := M)
    (∑ x ∈ s with
      Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x ∨ Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x,
      g x • v x)
    0
⊢ 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
have rw₁ : Disjoint ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x})
  ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x})
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
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
have this : HAdd.hAdd (α := 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)) =
  0
Tactic: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
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
have 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))
Tactic: rw [← eq_neg_iff_add_eq_zero] at this
Cleared hypotheses: this
-- 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
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
have refine_2 : ∀
  (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 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))),
  g i = 0
Tactic: rw [disjoint_def'] at hlr
Cleared hypotheses: hlr, s, g, hg, i, hi, this
-- 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
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))
⊢ Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0
have refine_1 : ∀ i ∈ s.preimage Sum.inl sorry,
  Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
Tactic: refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
-- 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
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))
refine_1 :
  ∀ i ∈ s.preimage Sum.inl ⋯,
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
⊢ Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0
have refine_2 : ∀ i ∈ s.preimage Sum.inr sorry,
  Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
Tactic: refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
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
have A : Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl sorry, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0
Tactic: 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⟩)
-- 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
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
have refine_2 : ∀ (i : ι) (hi : Sum.inl i ∈ s), g (Sum.inl i) = 0
Tactic: rcases i with i | i
Cleared hypotheses: i, hi
-- 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
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
refine_2 : ∀ (i : ι) (hi : Sum.inl i ∈ s), g (Sum.inl i) = 0
⊢ g i = 0
have refine_2₁ : ∀ (i : ι') (hi : Sum.inr i ∈ s), g (Sum.inr i) = 0
Tactic: rcases i with i | i
Cleared hypotheses: i, hi
-- 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
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.inr i ∈ s
⊢ g (Sum.inr i) = 0
have refine_2 : ∀ (A : Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inr sorry, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) 0) (i : ι')
  (hi : Sum.inr i ∈ s), g (Sum.inr i) = 0
Tactic: rw [this, neg_eq_zero] at A
Cleared hypotheses: A, i, hi
-- 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
⊢ 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 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)))
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)
-- 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)))
⊢ 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 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))
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)
-- 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))
⊢ 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_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))
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)
-- 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))
⊢ 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 : 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
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)