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
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
⊢ 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 : 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
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 (hypothesis)
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))
⊢ LinearIndepOn R v (s ∪ t)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
⊢ 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 : ι)))
have rwa : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (range fun (x : (↑t : Type u')) ↦ v (↑x : ι)))
Tactic: rwa [← image_eq_range, ← image_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ LinearIndepOn R v (s ∪ t)
have 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 : ι))
Tactic: have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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 : ι))
⊢ LinearIndepOn R v (s ∪ t)
have hdj₁ : Disjoint s t
Tactic: have hdj := (hdj.of_span₀ hs.zero_notMem_image).of_image
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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} R (M := M) fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)
have h : ∀ (x : ι) (hx : x ∈ s),
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
    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 sorry)
Tactic: convert! (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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 ⋯)
⊢ LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)
have h₁ : ∀ (x : ι) (hx : x ∈ t),
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
    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 sorry)
Tactic: convert! (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
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 ⋯)
have h : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  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 sorry))
Tactic: rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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 ⋯))
⊢ 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 ⋯)
have h₁ : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  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 sorry) : ι) hx))
Tactic: rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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))
⊢ 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 ⋯)
have h₂ : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) hx) : ι)
Tactic: rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
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 ⋯)
have h : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  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 sorry))
Tactic: rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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 ⋯))
⊢ 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 ⋯)
have h₁ : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  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 sorry) : ι) hx))
Tactic: rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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))
⊢ 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 ⋯)
have h₂ : v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) =
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) x sorry) : ι) hx) : ι)
Tactic: rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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))
have refine : ∀ (h : LinearIndepOn R v (s ∪ 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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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 (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
have h₁ : v '' s = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' s
Tactic: convert! h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
⊢ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
have h₂ : v '' t = (fun (x : (↑(s ∪ t) : Type u')) ↦ v (↑x : ι)) '' Subtype.val (p := fun (x : ι) ↦ x ∈ s ∪ t) ⁻¹' t
Tactic: convert! h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
⊢ LinearIndepOn R id (s ∪ t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
have 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)
Tactic: rw [linearIndepOn_union_iff hdj, image_id, image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
⊢ LinearIndepOn R id (s ∪ t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
have 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)
Tactic: rw [linearIndepOn_union_iff hdj, image_id, image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
⊢ LinearIndepOn R id (s ∪ t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (α := Submodule R M) (span R s) (span R t)
have 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)
Tactic: rw [linearIndepOn_union_iff hdj, image_id, image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
⊢ LinearIndependent L (M := G → L) fun (f : G →* L) ↦ (⇑f : (a : G) → L)
have apply : ∀ (s : Finset (G →* L)) (g : (G →* L) → L),
  Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
Tactic: apply linearIndependent_iff'.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
have h : ∀ (x : G),
  HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x
have h : HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x - HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x =
  0
Tactic: rw [← sub_eq_zero]