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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
⊢ hv.repr.range = ⊤
have rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).range = ⊤
Tactic: rw [LinearIndependent.repr, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).range = ⊤
⊢ hv.repr.range = ⊤
have rw₁ : Eq (α := Submodule R (ι →₀ R)) ⊤ ⊤
Tactic: rw [LinearIndependent.repr, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
⊢ (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x = l
have this : Eq.{u_4 + 1} (α := M)
  ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) : M) :
    M)
  ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
Tactic: have :
    ↑((LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l) =
      Finsupp.linearCombination R v l :=
    rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
⊢ ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
have this₁ : (↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) : M) =
  (↑x : M)
Tactic: rw [eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
⊢ (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x = l
have this₁ : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
Tactic: have : (LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x := by
    rw [eq] at this
    exact Subtype.ext_iff.2 this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this_1 :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
this : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
⊢ (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x = l
have rw : Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R)
  ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
      ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
    ι →₀ R)
Tactic: rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this_1 :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
this : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
⊢ Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R)
    ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
        ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)
have rw : Eq (α := ι →₀ R)
  ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R)
      (((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
    ι →₀ R)
  ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
      ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
    ι →₀ R)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
i : ι
x : ↥(span R (range v))
hx : (↑x : M) = v i
⊢ Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)
have apply : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) = (↑x : M)
Tactic: apply hv.repr_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : Nontrivial R
x : ↥(span R (range v))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x
have a : Eq.{u_4 + 1} (α := ↥(span R (range v)))
  ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
      (Finsupp.equivMapDomain (Equiv.ofInjective v sorry).symm (Span.repr R (range v) x)) :
    ↥(span R (range v)))
  ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
    ↥(span R (range v)))
Tactic: apply (LinearIndependent.linearCombinationEquiv hv).injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : Nontrivial R
x : ↥(span R (range v))
⊢ Eq.{u_4 + 1} (α := ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) :
      ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
      ↥(span R (range v)))
have a : Eq.{u_4 + 1} (α := M)
  (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        (Finsupp.equivMapDomain (Equiv.ofInjective v sorry).symm (Span.repr R (range v) x))) :
    M)
  (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)) :
    M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
inst_3 : Nontrivial R
x : ↥(span R (range v))
⊢ Span.repr R (range v) x =
    Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)
have p : Finsupp.equivMapDomain (Equiv.ofInjective v sorry).symm (Span.repr R (range v) x) =
  (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x
Tactic: have p :
    (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm =
      hv.repr x := by
    apply (LinearIndependent.linearCombinationEquiv hv).injective
    ext
    simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
      LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
      Span.finsupp_linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : Nontrivial R
x : ↥(span R (range v))
p :
  Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x
⊢ Span.repr R (range v) x =
    Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)
have h : ∀ (i : ι),
  Eq.{u_2 + 1} (α := R)
    ((Span.repr R (range v) x : (a : (↑(range v) : Type u_4)) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) sorry) :
      R)
    ((Finsupp.equivMapDomain (Equiv.ofInjective v sorry) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
          (a : (↑(range v) : Type u_4)) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) sorry) :
      R)
Tactic: ext ⟨_, ⟨i, rfl⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
i : ι
a : R
ha : Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i)
⊢ a = 0
have ha₁ : ∃ (y : ι →₀ R),
  Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) y ∧
    (Finsupp.linearCombination R v : (a : ι →₀ R) → M) y = a • v i
Tactic: rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
i : ι
a : R
ha :
  ∃ (y : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) y ∧
      (Finsupp.linearCombination R v : (a : ι →₀ R) → M) y = a • v i
⊢ a = 0
have rcases : ∀ (l : ι →₀ R) (hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l)
  (e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i), a = 0
Tactic: rcases ha with ⟨l, hl, e⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
⊢ a = 0
have hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
Tactic: rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl
Cleared hypotheses: hl, e
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
⊢ a = 0
have by_contra : ∀ (hn : ¬a = 0), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
⊢ i.Maximal ↔ ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
have mp : i.Maximal → ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
mp : i.Maximal → ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
⊢ i.Maximal ↔ ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
have mpr : (∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j) → i.Maximal
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : i.Maximal
⊢ Surjective j
have p₁ : range (w ∘ j) = range w
Tactic: specialize p (range w) i'.linearIndepOn_id (range_comp_subset_range _ _)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j
have p₁ : w '' range j = w '' univ
Tactic: rw [range_comp, ← image_univ (f := w)] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
⊢ (Function.comp (β := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) fun (i : ι) ↦
      Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯) =
    v
have h₁ : ∀ (x : ι),
  Function.comp (β := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w))
      (fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) sorry) x =
    v x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
⊢ range v = w
have p₁ : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) sorry
Tactic: specialize
      p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
        (by
          ext
          simp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
p : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯
⊢ range v = w
have q : Eq.{v + 1} (α := Set M)
  ((fun (s : Set { x : M // x ∈ w }) ↦ Subtype.val (p := fun (x : M) ↦ x ∈ w) '' s)
    (range fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) sorry))
  ((fun (s : Set { x : M // x ∈ w }) ↦ Subtype.val (p := fun (x : M) ↦ x ∈ w) '' s) univ)
Tactic: have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
p : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯
q :
  Eq.{v + 1} (α := Set M)
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w))
      (range fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯))
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) univ)
⊢ range v = w
have q₁ : Eq.{v + 1} (α := Set M) ((fun (x : ι) ↦ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v x) sorry) : M)) '' univ)
  (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) univ)
Tactic: rw [← image_univ, image_image] at q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this : Sub R := CanonicallyOrderedAdd.toSub
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have this₁ : OrderedSub R
Tactic: haveI : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have rw : (∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Tactic: rw [linearIndependent_iff'ₛ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_1 : ∀
  (h :
    ∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
  (s t : Finset ι) (f : ι → R) (hst : Disjoint s t)
  (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)), (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Tactic: refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (s t : Finset ι) (f : ι → R) (hst : Disjoint s t)
    (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)), (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_2 : ∀
  (h :
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0)
  (s : Finset ι) (f g : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)),
  ∀ i ∈ s, f i = g i
Tactic: refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_1 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ s then f i else 0) i) (v i))
  (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t then f i else 0) i) (v i))
Tactic: specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)
refine_1 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ s then f i else 0) i) (v i))
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t then f i else 0) i) (v i))
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_1₁ : ∀ (h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0), (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Tactic: specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
Cleared hypotheses: h