awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))
have h : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i}))
  (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l)
Tactic: refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
h :
  Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i}))
    (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))
have h₁ : (Finsupp.linearCombination R v : (a : ι →₀ R) → M)
    (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l) =
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i)
Tactic: refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i}))
    (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l)
have h : ∀ x ∉ univ \ {i},
  Eq.{u_2 + 1} (α := R)
    ((HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l : (a : ι) → R) x : R) (0 : R)
Tactic: rw [Finsupp.mem_supported']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
j : ι
hj : j ∉ univ \ {i}
⊢ Eq.{u_2 + 1} (α := R)
    ((HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l : (a : ι) → R) j : R) (0 : R)
have hij : j = i
Tactic: have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_diff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
have apply : (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) ↔
  ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
Tactic: apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
⊢ (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) ↔
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
have mp : (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) →
  ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
mp :
  (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) →
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
⊢ (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) ↔
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
have mpr : (∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))) →
  ∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
ha : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i)
⊢ a = 0
have mpr : ∀ (ha' : ¬a = 0), False
Tactic: by_contra ha'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s : Set ι
⊢ LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
have rw : (∀ (i : (↑s : Type u')),
    v (↑i : ι) ∉ span K (image (α := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
  ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Tactic: rw [LinearIndepOn, linearIndependent_iff_notMem_span, ← Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : (↑s : Type u')),
      v (↑i : ι) ∉ span K (image (α := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
    ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
have simp_rw : (∀ (i : (↑s : Type u')),
    v (↑i : ι) ∉ span K (v '' image (α := (↑s : Type u')) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
  ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Tactic: simp_rw [Set.image_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
have simp : (FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_1 : Fin 2 → R) ↦
    FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_2 : Fin 2 → R) ↦
      x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
  ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
Tactic: simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ t = 0
have suffices : s = 0 ∧ 0 = t
Tactic: suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ s = 0 ∧ t = 0
have refine_2 : ∀ (h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0), s = 0 ∧ t = 0
Tactic: replace h := @h (.single 0 s + .single 1 t) 0 ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
refine_2 :
  ∀ (h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0), s = 0 ∧ t = 0
⊢ s = 0 ∧ t = 0
have refine_1 : Eq.{u_4 + 1} (α := M)
  ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M)
      (HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t)) :
    M)
  ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M) 0 : M)
Tactic: replace h := @h (.single 0 s + .single 1 t) 0 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
⊢ LinearIndepOn R v (⋃ (i : η), s i)
have pos : ∀ (hη : Nonempty η), LinearIndepOn R v (⋃ (i : η), s i)
Tactic: by_cases hη : Nonempty η
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
pos : ∀ (hη : Nonempty η), LinearIndepOn R v (⋃ (i : η), s i)
⊢ LinearIndepOn R v (⋃ (i : η), s i)
have neg : ∀ (hη : ¬Nonempty η), LinearIndepOn R v (⋃ (i : η), s i)
Tactic: by_cases hη : Nonempty η
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
⊢ LinearIndepOn R v (⋃ (i : η), s i)
have pos : ∀ (t : Set ι) (ht : t ⊆ ⋃ (i : η), s i) (ft : t.Finite), LinearIndepOn R v t
Tactic: refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
⊢ LinearIndepOn R v t
have pos : ∀ (I : Set η) (fi : I.Finite) (hI : t ⊆ ⋃ i ∈ I, s i), LinearIndepOn R v t
Tactic: rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndepOn R v t
have pos : ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i), LinearIndepOn R v t
Tactic: rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ LinearIndepOn R v (⋃ (i : η), s i)
have neg : Subset.{u'} (α := Set ι) (⋃ (x : η), s x) ∅
Tactic: refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Set ι)
hs : DirectedOn (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃₀ s)
have rw : LinearIndepOn R v (⋃ (i : (↑s : Type u')), (↑i : Set ι))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ a ∈ s, t a)
have rw : LinearIndepOn R v (⋃ (x : (↑s : Type u_6)), t (↑x : η))
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ iSupIndep (α := Submodule R (ι →₀ M)) fun (i : ι) ↦ LinearMap.range (Finsupp.lsingle i)
have refine : ∀ (i : ι),
  LE.le (α := Submodule R (ι →₀ M))
    ((fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) i ⊓
      ⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j)
    ⊥
Tactic: refine fun i ↦ disjoint_iff_inf_le.mpr ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
this :
  LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)
⊢ Membership.mem (α := ι →₀ M) (γ := Submodule R (ι →₀ M)) ⊥ ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
have this₁ : (↑(Finsupp.support.{u', u_4} (M := M) ((Finsupp.lsingle i : (a : M) → ι →₀ M) m)) : Set ι) ⊆ {i}ᶜ
Tactic: have := (Finsupp.mem_supported ..).mp (this hm)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
⊢ Membership.mem (α := ι →₀ M) (γ := Submodule R (ι →₀ M)) ⊥ ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
have suffices : LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
  (Finsupp.supported M R {i}ᶜ)
Tactic: suffices ⨆ j ≠ i, LinearMap.range (Finsupp.lsingle j) ≤ Finsupp.supported M R {i}ᶜ by
    have := (Finsupp.mem_supported ..).mp (this hm); simp_all
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
⊢ LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)
have refine : ∀ (j : ι) (ne : j ≠ i),
  LE.le (α := Submodule R (ι →₀ M)) (LinearMap.range (Finsupp.lsingle j)) (Finsupp.supported M R {i}ᶜ)
Tactic: refine iSup₂_le fun j ne ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : iSupIndep m
⊢ iSupIndep.{u' + 1, u_5} (α := Submodule R M') fun (i : ι) ↦ map f (m i)
have simp_rw : ∀ (ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥) (i : ι),
  map f (m i) ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j) ≤ ⊥
Tactic: simp_rw [iSupIndep, disjoint_iff_inf_le] at ind ⊢
Cleared hypotheses: ind
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
⊢ Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') x : M')
have rw : Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') 0 : M')
Tactic: rw [ind i ⟨hxi, _⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
rw : Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') 0 : M')
⊢ Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') x : M')
have rw₁ : x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
Tactic: rw [ind i ⟨hxi, _⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
⊢ x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
have hx₁ : Membership.mem (α := M') (↑(map f (⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1)) : Set M') ((f : (a : M) → M') x : M')
Tactic: simp_rw [← Submodule.map_iSup] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(map f (⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1)) : Set M') ((f : (a : M) → M') x : M')
⊢ x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
have have : ∀ (y : M) (hy : y ∈ (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1) : Set M))
  (eq : Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') y : M') ((f : (a : M) → M') x : M')),
  x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
Tactic: have ⟨y, hy, eq⟩ := hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
⊢ iSupIndep.{u' + 1, u_4} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
have h : ∀ (x : ι),
  Eq (α := Submodule R M) (R ∙ v x)
    (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x)))
Tactic: convert! LinearMap.iSupIndep_map _ hv (iSupIndep_range_lsingle ι R R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
x : ι
⊢ Eq (α := Submodule R M) (R ∙ v x)
    (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x)))
have h : ∀ (x_1 : M),
  Membership.mem (γ := Submodule R M) (R ∙ v x) x_1 ↔
    Membership.mem (γ := Submodule R M)
      (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x))) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
have h : ∀ (val : ι),
  Eq.{u_4 + 1} (α := M)
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).1
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).1
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
h :
  ∀ (val : ι),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
have h₁ : ∀ (val : ι),
  Eq.{u_5 + 1} (α := M')
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).2
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).2
Tactic: ext (_ | _)