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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have rcases : ∀ (i' : ι')
  (hi' :
    repr
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
            (v i) sorry) =
        Finsupp.single i' 1 ∧
      (f : (a : ι') → ι) i' = i),
  ∃ (a : ι'), (f : (a : ι') → ι) a = i
Tactic: rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
i' : ι'
hi' :
  repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯) =
      Finsupp.single i' 1 ∧
    (f : (a : ι') → ι) i' = i
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have h : (f : (a : ι') → ι) i' = i
Tactic: use i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
have apply : (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ⊆
  (↑(span R
        (range (ι := (↑t : Type u_4))
          ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))))) :
    Set M)
Tactic: apply surjective_of_linearIndependent_of_span hs f _
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ⊆
    (↑(span R
          (range (ι := (↑t : Type u_4))
            ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))))) :
      Set M)
have h₁ : (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) = s
Tactic: convert! hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h₁ : (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) = s
⊢ (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ⊆
    (↑(span R
          (range (ι := (↑t : Type u_4))
            ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))))) :
      Set M)
have h₂ : range (ι := (↑t : Type u_4))
    ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))) =
  t
Tactic: convert! hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ s = t
have h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
Tactic: have h_surj : Surjective f := by
    apply surjective_of_linearIndependent_of_span hs f _
    convert! hst <;> simp [f, comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
⊢ s = t
have apply : s ⊆ t
Tactic: apply Subset.antisymm _ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
⊢ x ∈ t
have rcases : ∀ (y : (↑t : Type u_4))
  (hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx), x ∈ t
Tactic: rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
y : (↑t : Type u_4)
hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
⊢ x ∈ t
have h₁ : x = (↑y : M)
Tactic: convert! y.mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
y : (↑t : Type u_4)
hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
⊢ x = (↑y : M)
have h₁ : (↑y : M) = (↑y : M)
Tactic: rw [← Subtype.mk.inj hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : LE.le (α := Submodule R M) (span R s) (span R t)
⊢ s ⊆ t
have this : s ∪ t = t
Tactic: have :=
    eq_of_linearIndepOn_id_of_span_subtype (hl.mono (Set.union_subset hsu htu))
      Set.subset_union_right (Set.union_subset (Set.Subset.trans subset_span hst) subset_span)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : LE.le (α := Submodule R M) (span R s) (span R t)
this : s ∪ t = t
⊢ s ⊆ t
have rw : s ⊆ s ∪ t
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i)
i : ι
⊢ f i = g i
have rw : ∀ (heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x • v x - g x • v x)) 0) (i : ι), f i = g i
Tactic: rw [← sub_eq_zero, ← sum_sub_distrib] at heq
Cleared hypotheses: heq, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x • v x - g x • v x)) 0
i : ι
⊢ f i = g i
have heq₁ : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x - g x) • v x) 0
Tactic: simp_rw [← sub_smul] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (range v)) f.ker
have simp_rw : Disjoint (α := Submodule R M) (span R (range v)) ⊥
Tactic: simp_rw [hf_inj, disjoint_bot_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
have rw : ∀ (hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) (i : R' → R)
  (j : M →+ M') (hi : ∀ (r : R'), i r = 0 → r = 0)
  (hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0)
  (hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M'))
  (s : Finset ι) (g : ι → R'),
  Eq.{u_7 + 1} (α := M') (∑ i ∈ s, HSMul.hSMul (β := M') (g i) (((⇑j : (a : M) → M') ∘ v) i)) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_iff'] at hv ⊢
Cleared hypotheses: hv, i, j, hi, hj, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
S : Finset ι
r' : ι → R'
H : Eq.{u_7 + 1} (α := M') (∑ i ∈ S, HSMul.hSMul (β := M') (r' i) (((⇑j : (a : M) → M') ∘ v) i)) 0
s : ι
hs : s ∈ S
⊢ r' s = 0
have H₁ : Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') (∑ x ∈ S, i (r' x) • v x) : M') (0 : M')
Tactic: simp_rw [comp_apply, ← hc, ← map_sum] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (Set.range v)) f.ker
have simp_rw : Disjoint (α := Submodule R M) (span R (Set.range v)) ⊥
Tactic: simp_rw [hf_inj, disjoint_bot_right]
-- 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
m : ℕ
x : M
v : Fin m → M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v)
have rw : ∀ (hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0)
  (x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0)
  (g : Fin (m + 1) → R),
  Eq.{u_4 + 1} (α := M)
      (∑ i : Fin (m + 1), HSMul.hSMul (β := M) (g i) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v i : M)) 0 →
    ∀ (i : Fin (m + 1)), g i = 0
Tactic: rw [Fintype.linearIndependent_iff] at hli ⊢
Cleared hypotheses: hli, x_ortho
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
total_eq :
  Eq.{u_4 + 1} (α := M)
    (∑ i : Fin (m + 1), HSMul.hSMul (β := M) (g i) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v i : M)) 0
j : Fin (m + 1)
⊢ g j = 0
have total_eq₁ : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
Tactic: simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq
Cleared hypotheses: total_eq
-- 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
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g 0 = 0
have refine : Membership.mem (γ := Submodule R M) (span R (range v)) (∑ i : Fin m, g i.succ • v i)
Tactic: refine x_ortho (g 0) (∑ i : Fin m, g i.succ • v i) ?_ total_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g j = 0
have this : g 0 = 0
Tactic: have : g 0 = 0 := by
    refine x_ortho (g 0) (∑ i : Fin m, g i.succ • v i) ?_ total_eq
    exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0
have total_eq₁ : Eq.{u_4 + 1} (α := M) (∑ x : Fin m, g x.succ • v x) 0
Tactic: rw [this, zero_smul, zero_add] at total_eq
Cleared hypotheses: total_eq, this
-- 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
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin m.succ) ↦ M) v x)
have rw : LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M)
  (Function.comp (β := Fin (m + 1)) (Fin.cons (α := fun (x : Fin (m + 1)) ↦ M) x v)
    (⇑(finRotate (m + 1)) : (a : Fin (m + 1)) → Fin (m + 1)))
Tactic: rw [Fin.snoc_eq_cons_rotate v x, ← Function.comp_def]
-- 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 (v '' range Sum.inr))
Tactic: rw [range_comp v, range_comp v]
-- 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 (v '' range Sum.inl)) (span R (v '' range 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: refine ⟨?_, ?_⟩
-- 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
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 (v '' range Sum.inl)) (span R (v '' range 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: refine ⟨?_, ?_⟩
-- 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
h : 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))
have refine_1 : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
Tactic: refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
-- 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 : 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
have refine_2 : ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
  (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
  (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)))
  (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_iff'] at *
Cleared hypotheses: hl, hr, hlr
-- 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
⊢ 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 : 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
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]