awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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_1 : ι ⊕ ι'
hi : i_1 ∈ 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))
i : ι'
h : i ∈ s.preimage Sum.inr ⋯
⊢ Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))

Tactic:
smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)

Premises used: Set.mem_range_self, Set.Mem, Sum.inr, And.intro, Exists.intro, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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_1 : ι ⊕ ι'
hi : i_1 ∈ 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))
i : ι'
h : i ∈ s.preimage Sum.inr ⋯
⊢ Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))

Tactic:
exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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

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⟩)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_2₁ : ∀ (i : ι') (hi : Sum.inr i ∈ s), g (Sum.inr i) = 0
⊢ g i = 0

Tactic:
rcases i with i | i
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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.inl i ∈ s
⊢ g (Sum.inl i) = 0

Tactic:
hl _ _ A i (Finset.mem_preimage.2 hi)

Premises used: Iff.mpr, Finset.mem_preimage
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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.inl i ∈ s
⊢ g (Sum.inl i) = 0

Tactic:
exact hl _ _ A i (Finset.mem_preimage.2 hi)

Premises used: Iff.mpr, Finset.mem_preimage
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_2 :
  ∀ (A : Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) 0) (i : ι')
    (hi : Sum.inr i ∈ s), g (Sum.inr i) = 0
⊢ g (Sum.inr i) = 0

Tactic:
rw [this, neg_eq_zero] at A

Premises used: neg_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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) (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0

Tactic:
hr _ _ A i (Finset.mem_preimage.2 hi)

Premises used: Iff.mpr, Finset.mem_preimage
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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) (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0

Tactic:
exact hr _ _ A i (Finset.mem_preimage.2 hi)

Premises used: Iff.mpr, Finset.mem_preimage
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v' : ι' → M
hv : LinearIndependent R v
hv' : LinearIndependent R v'
h : Disjoint (α := Submodule R M) (span R (range v)) (span R (range v'))
⊢ LinearIndependent R (Sum.elim v v')

Tactic:
linearIndependent_sum.2 ⟨hv, hv', h⟩

Premises used: Iff.mpr, linearIndependent_sum, And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h : Nontrivial R
rwa : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (range fun (x : (↑t : Type u')) ↦ v (↑x : ι)))
rwa₁ rwa₂ rwa₃ rwa₄ : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
⊢ Disjoint.{u_4} (α := Submodule R M) (span R (range fun (x : (↑s : Type u')) ↦ v (↑x : ι)))
    (span R (range fun (x : (↑t : Type u')) ↦ v (↑x : ι)))

Tactic:
rwa [← image_eq_range, ← image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h : Nontrivial R
⊢ LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))

Tactic:
have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h : Nontrivial R
hli :
  LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
⊢ Disjoint s t

Tactic:
have hdj := (hdj.of_span₀ hs.zero_notMem_image).of_image
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj_1 : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h : Nontrivial R
hli :
  LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
hdj : Disjoint s t
⊢ LinearIndependent.{u', u_2, u_4} (ι := (↑(s ∪ t) : Type u')) R (M := M)
    (comp (β := (↑s : Type u') ⊕ (↑t : Type u'))
      (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      (⇑(Equiv.Set.union (s := s) (t := t) hdj) : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u')))

Tactic:
(hli.comp _ (Equiv.Set.union hdj).injective)

Premises used: Equiv.Set.union, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj_1 : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h_1 : Nontrivial R
hli :
  LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
hdj : Disjoint s t
h :
  ∀ (x : ι) (hx : x ∈ s),
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
      comp (α := (↑(s ∪ t) : Type u')) (β := (↑s : Type u') ⊕ (↑t : Type u'))
        (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
        (⇑(Equiv.Set.union (s := s) (t := t) hdj) : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯)
h₁ :
  ∀ (x : ι) (hx : x ∈ t),
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
      comp (α := (↑(s ∪ t) : Type u')) (β := (↑s : Type u') ⊕ (↑t : Type u'))
        (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
        (⇑(Equiv.Set.union (s := s) (t := t) hdj) : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯)
⊢ LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)

Tactic:
convert! (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩

Premises used: Equiv.Set.union, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj_1 : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h_1 : Nontrivial R
hli :
  LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
hdj : Disjoint s t
x : ι
hx : x ∈ s
h :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) (fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      ((Equiv.Set.union (s := s) (t := t) hdj : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯))
h₁ :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) (fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) hx))
h₂ h₃ :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) hx) : ι)
⊢ v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    comp (α := (↑(s ∪ t) : Type u')) (β := (↑s : Type u') ⊕ (↑t : Type u'))
      (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      (⇑(Equiv.Set.union (s := s) (t := t) hdj) : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯)

Tactic:
rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]

Premises used: Equiv.Set.union_apply_left, Sum.elim_inl, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj_1 : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
h_1 : Nontrivial R
hli :
  LinearIndependent.{u', u_2, u_4} (ι := (↑s : Type u') ⊕ (↑t : Type u')) R (M := M)
    (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
hdj : Disjoint s t
x : ι
hx : x ∈ t
h :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) (fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      ((Equiv.Set.union (s := s) (t := t) hdj : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯))
h₁ :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) (fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) hx))
h₂ h₃ :
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) hx) : ι)
⊢ v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯) : ι) =
    comp (α := (↑(s ∪ t) : Type u')) (β := (↑s : Type u') ⊕ (↑t : Type u'))
      (Sum.elim (fun (x : (↑s : Type u')) ↦ v (↑x : ι)) fun (x : (↑t : Type u')) ↦ v (↑x : ι))
      (⇑(Equiv.Set.union (s := s) (t := t) hdj) : (a : (↑(s ∪ t) : Type u')) → (↑s : Type u') ⊕ (↑t : Type u'))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x ⋯)

Tactic:
rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]

Premises used: Sum.elim_inr, Function.comp_apply, Equiv.Set.union_apply_right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hdj : Disjoint (α := Submodule R M) (span R s) (span R t)
⊢ Disjoint (α := Submodule R M) (span R (id '' s)) (span R (id '' t))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
⊢ LinearIndepOn R v (s ∪ t) ↔
    LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩,
    fun h ↦ h.1.union h.2.1 h.2.2⟩

Premises used: Set.subset_union_right, Set.subset_union_left, LinearIndepOn.union, LinearIndepOn.mono, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
refine : ∀ (h : LinearIndepOn R v (s ∪ t)), Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
⊢ LinearIndepOn R v (s ∪ t) ↔
    LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
refine ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩,
    fun h ↦ h.1.union h.2.1 h.2.2⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ Disjoint.{u_4} (α := Submodule R M)
    (span R ((fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' s))
    (span R ((fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' t))

Tactic:
h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _)

Premises used: LinearIndependent.disjoint_span_image, Disjoint.preimage
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
h₁ : v '' s = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' s
h₂ : v '' t = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' t
⊢ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
convert! h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _)

Premises used: LinearIndependent.disjoint_span_image
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' s = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' s

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' t = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' t

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set M
hdj : Disjoint s t
rw :
  LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R (id '' s)) (span R (id '' t)) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
rw₁ :
  LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R (id '' t)) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
rw₂ rw₃ :
  LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
⊢ LinearIndepOn R id (s ∪ t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)

Tactic:
rw [linearIndepOn_union_iff hdj, image_id, image_id]

Premises used: linearIndepOn_union_iff, Set.image_id