awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
inr : #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ False

Tactic:
suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)

Tactic:
lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_

Premises used: lt_of_le_of_lt, Cardinal.mk_iUnion_le_sum_mk, Cardinal.sum_le_sum, Cardinal.aleph0, le_trans
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
inr : ∀ (i : (↑J : Type v)), #(↑(S' i) : Type v) ≤ (fun (x : (↑J : Type v)) ↦ ℵ₀) i
inr₁ : (sum fun (x : (↑J : Type v)) ↦ ℵ₀) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)

Tactic:
refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_

Premises used: lt_of_le_of_lt, Cardinal.mk_iUnion_le_sum_mk, Cardinal.sum_le_sum, Cardinal.aleph0, le_trans
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ ∀ (i : (↑J : Type v)), #(↑(S' i) : Type v) ≤ (fun (x : (↑J : Type v)) ↦ ℵ₀) i

Tactic:
fun j => (Cardinal.lt_aleph0_of_finite _).le

Premises used: Set.Elem, LT.lt.le, Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ ∀ (i : (↑J : Type v)), #(↑(S' i) : Type v) ≤ (fun (x : (↑J : Type v)) ↦ ℵ₀) i

Tactic:
exact fun j => (Cardinal.lt_aleph0_of_finite _).le

Premises used: LT.lt.le, Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
this : Nontrivial R
val : Infinite.{v + 1} (↑J : Type v)
S : (↑J : Type v) → Set ι :=
  fun (j : (↑J : Type v)) ↦ (↑(Finsupp.support.{w, u} (M := R) ((v.repr : (a : M) → ι →₀ R) (↑j : M))) : Set ι)
S' : (↑J : Type v) → Set M := fun (j : (↑J : Type v)) ↦ (⇑v : (a : ι) → M) '' S j
hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ (sum fun (x : (↑J : Type v)) ↦ ℵ₀) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f : (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
i₁ :
  Injective (α := ι →₀ R) (β := Finsupp.{v, u} (↑w : Type v) R)
    (⇑(linearCombination R fun (i : ι) ↦
          Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯)) :
      (a : ι →₀ R) → (↑w : Type v) →₀ R)
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
fapply card_le_of_injective' R

Premises used: card_le_of_injective'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f : ι → Finsupp.{v, u} (↑w : Type v) R
⊢ (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R

Tactic:
apply Finsupp.linearCombination

Premises used: Finsupp.linearCombination
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
⊢ ι → Finsupp.{v, u} (↑w : Type v) R

Tactic:
exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩

Premises used: Set.mem_range_self, Span.repr, Subtype.mk
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f g : ι →₀ R
h :
  Eq (α := Finsupp.{v, u} (↑w : Type v) R)
    ((linearCombination R fun (i : ι) ↦
            Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
          (a : ι →₀ R) → (↑w : Type v) →₀ R)
        f :
      Finsupp.{v, u} (↑w : Type v) R)
    ((linearCombination R fun (i : ι) ↦
            Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
          (a : ι →₀ R) → (↑w : Type v) →₀ R)
        g :
      Finsupp.{v, u} (↑w : Type v) R)
⊢ Eq.{v + 1} (α := M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            f :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            g :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)

Tactic:
apply_fun linearCombination R ((↑) : w → M) at h

Premises used: Finsupp.linearCombination, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            f :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            g :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
⊢ Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)

Tactic:
simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h

Premises used: Span.finsupp_linearCombination_repr, Finsupp.linearCombination_linearCombination
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)
⊢ f = g

Tactic:
i h
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst_5 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)
⊢ f = g

Tactic:
exact i h
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Finite.{v + 1} (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this : Fintype (↑w : Type v) := Fintype.ofFinite (↑w : Type v)
t : Finset ι
v' : (x : (↑(↑t : Set ι) : Type u_2)) → M := fun (x : (↑(↑t : Set ι) : Type u_2)) ↦ v (↑x : ι)
⊢ LinearIndependent R v'

Tactic:
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Finite.{v + 1} (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this : Fintype (↑w : Type v) := Fintype.ofFinite (↑w : Type v)
t : Finset ι
v' : (x : (↑(↑t : Set ι) : Type u_2)) → M := fun (x : (↑(↑t : Set ι) : Type u_2)) ↦ v (↑x : ι)
i' : LinearIndependent R v'
⊢ range v' ≤ (↑(span R w) : Set M)

Tactic:
have s' : range v' ≤ span R w := (range_comp_subset_range _ _).trans s
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Finite.{v + 1} (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this : Fintype (↑w : Type v) := Fintype.ofFinite (↑w : Type v)
t : Finset ι
v' : (x : (↑(↑t : Set ι) : Type u_2)) → M := fun (x : (↑(↑t : Set ι) : Type u_2)) ↦ v (↑x : ι)
i' : LinearIndependent R v'
s' : range v' ≤ (↑(span R w) : Set M)
⊢ t.card ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
simpa using linearIndependent_le_span_aux' v' i' w s'

Premises used: linearIndependent_le_span_aux'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
⊢ Finite ι

Tactic:
haveI : Finite ι := i.finite_of_le_span_finite v w s
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
rw :
  LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
    (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})

Tactic:
rw [Cardinal.mk_fintype]

Premises used: Cardinal.mk_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
simp : Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
    (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})

Tactic:
simp only [Nat.cast_le]

Premises used: Nat.cast_le
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
linearIndependent_le_span_aux' v i w s

Premises used: linearIndependent_le_span_aux'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
exact linearIndependent_le_span_aux' v i w s

Premises used: linearIndependent_le_span_aux'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
apply : range v ≤ (↑(span R w) : Set M)
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})

Tactic:
apply linearIndependent_le_span' v i w

Premises used: linearIndependent_le_span'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
rw : range v ≤ (↑⊤ : Set M)
⊢ range v ≤ (↑(span R w) : Set M)

Tactic:
rw [s]
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ range v ≤ (↑⊤ : Set M)

Tactic:
le_top

Premises used: Set.univ, setOf, le_top
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ range v ≤ (↑⊤ : Set M)

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Finset M
s : Eq (α := Submodule R M) (span R (↑w : Set M)) ⊤
⊢ #ι ≤ (↑w.card : Cardinal.{u_2})

Tactic:
simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s

Premises used: Finset.coe_sort_coe, linearIndependent_le_span, SetLike.coe, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
by_contra : ∀ (h : ¬#κ ≤ #ι), False
⊢ #κ ≤ #ι

Tactic:
by_contra h
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : ¬#κ ≤ #ι
⊢ #(Finset ι) < #κ

Tactic:
rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h

Premises used: not_le, Cardinal.mk_finset_of_infinite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
obtain : ∀ (s : Finset ι) (w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)), False
⊢ False

Tactic:
obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber' Φ h

Premises used: Cardinal.exists_infinite_fiber'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
s : Finset ι
w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ)
⊢ LinearIndependent R v'

Tactic:
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
s : Finset ι
w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
apply : range v' ≤ (↑(span R (↑(Finset.image (⇑b : (a : ι) → M) s) : Set M)) : Set M)
⊢ Finite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)

Tactic:
apply i'.finite_of_le_span_finite v' (s.image b)

Premises used: LinearIndependent.finite_of_le_span_finite, SetLike.coe, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
p : κ
w : Infinite.{w + 1} (↑(Φ ⁻¹' {Φ p}) : Type w)
v' : (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
simp :
  Membership.mem (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' (↑(Φ p) : Set ι)))
    (v' (Subtype.mk (p := fun (x : κ) ↦ x ∈ Φ ⁻¹' {Φ p}) p ⋯))
⊢ v' (Subtype.mk (p := fun (x : κ) ↦ x ∈ Φ ⁻¹' {Φ p}) p ⋯) ∈
    (↑(span R (↑(Finset.image (⇑b : (a : ι) → M) (Φ p)) : Set M)) : Set M)

Tactic:
simp only [SetLike.mem_coe, Finset.coe_image]

Premises used: Finset.coe_image, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
p : κ
w : Infinite.{w + 1} (↑(Φ ⁻¹' {Φ p}) : Type w)
v' : (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
⊢ Membership.mem (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' (↑(Φ p) : Set ι)))
    (v' (Subtype.mk (p := fun (x : κ) ↦ x ∈ Φ ⁻¹' {Φ p}) p ⋯))

Tactic:
apply Basis.mem_span_repr_support

Premises used: Module.Basis.mem_span_repr_support