awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
w : Set M
inst_5 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := M)
    (⇑(Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) : (a : (↑w : Type v) →₀ R) → M)
have i : Eq.{v + 1} (α := Submodule R M) (span R (range (ι := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w)))) ⊤
Tactic: rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
this : Nontrivial R
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have this₁ : Finite ι
Tactic: haveI := basis_finite_of_finite_spans w.toFinite s b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
this_1 : Nontrivial R
this : Finite ι
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have intro : ∀ (val : Fintype ι), #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
this_1 : Nontrivial R
this : Finite ι
val : Fintype ι
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have intro : LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
  (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
Tactic: rw [Cardinal.mk_fintype ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
this_1 : Nontrivial R
this : Finite ι
val : Fintype ι
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
    (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have intro : Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
Tactic: simp only [Nat.cast_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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) ⊤
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have inl : ∀ (val : Fintype (↑J : Type v)), #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
Tactic: cases fintypeOrInfinite J
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
inl : ∀ (val : Fintype (↑J : Type v)), #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have inr : Infinite.{v + 1} (↑J : Type v) → #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
Tactic: cases fintypeOrInfinite J
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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 : Fintype (↑J : Type v)
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have inl : lift.{v, w} #ι ≤ lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v})
Tactic: rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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 : Fintype (↑J : Type v)
⊢ lift.{v, w} #ι ≤ lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v})
have h : lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v}) =
  lift.{v, w} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{w})
Tactic: convert! Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have rcases : ∀ (i : ι) (hi : (v : (a : ι) → M) i = b), Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
Tactic: rcases mem_range.1 hb with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have this₁ : span R J ≤ comap (↑v.repr : M →ₗ[R] ι →₀ R) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
Tactic: have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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_1 : 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
this : span R J ≤ comap (↑v.repr : M →ₗ[R] ι →₀ R) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have this₁ : ⊤ ≤ comap (↑v.repr : M →ₗ[R] ι →₀ R) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
Tactic: rw [hJ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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_1 : 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
this : ⊤ ≤ comap (↑v.repr : M →ₗ[R] ι →₀ R) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have this₁ : Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
  ((v.repr : (a : M) → ι →₀ R) ((v : (a : ι) → M) i) : ι →₀ R)
Tactic: replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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_1 : 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
this :
  Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))
    ((v.repr : (a : M) → ι →₀ R) ((v : (a : ι) → M) i) : ι →₀ R)
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have this₁ : (↑{i} : Set ι) ⊆ ⋃ (j : (↑J : Type v)), S j
Tactic: rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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_1 : 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
this : (↑{i} : Set ι) ⊆ ⋃ (j : (↑J : Type v)), S j
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
have subst : ∀
  (hb :
    Membership.mem.{v, v} (α := M) (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M))
      ((v : (a : ι) → M) i : M)),
  Membership.mem.{v, v} (α := M) (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) ((v : (a : ι) → M) i : M)
Tactic: subst b
Cleared hypotheses: b, hb, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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_1 : 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
i : ι
this : (↑{i} : Set ι) ⊆ ⋃ (j : (↑J : Type v)), S j
hb :
  Membership.mem.{v, v} (α := M) (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) ((v : (a : ι) → M) i : M)
⊢ Membership.mem.{v, v} (α := M) (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) ((v : (a : ι) → M) i : M)
have rcases : ∀ (j : (↑J : Type v)) (hj : i ∈ S j),
  Membership.mem.{v, v} (α := M) (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) ((v : (a : ι) → M) i : M)
Tactic: rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have hs : Subset.{v} (α := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) (⋃ (j : (↑J : Type v)), S' j)
Tactic: have hs : range v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
have inr : ∀ (IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)), False
Tactic: refine le_of_not_gt fun IJ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
⊢ False
have inr : #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
Tactic: suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
have inr : ∀ (i : (↑J : Type v)), #(↑(S' i) : Type v) ≤ (fun (x : (↑J : Type v)) ↦ ℵ₀) i
Tactic: refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
have inr₁ : (sum fun (x : (↑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 _ => ℵ₀) ?_)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
have f : (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
Tactic: fapply card_le_of_injective' R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
have 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) sorry)) :
    (a : ι →₀ R) → (↑w : Type v) →₀ R)
Tactic: fapply card_le_of_injective' R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
⊢ (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
have f : ι → Finsupp.{v, u} (↑w : Type v) R
Tactic: apply Finsupp.linearCombination
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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)
⊢ f = g
have 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) sorry) :
            (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) sorry) :
            (a : ι →₀ R) → (↑w : Type v) →₀ R)
          g :
        Finsupp.{v, u} (↑w : Type v) R) :
    M)
Tactic: apply_fun linearCombination R ((↑) : w → M) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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)
⊢ f = g
have 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)
Tactic: simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
Cleared hypotheses: h