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
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) ⊤
f : Finsupp.{v, u} (↑w : Type v) R →ₗ[R] ι →₀ R
i :
  Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := ι →₀ R)
    (⇑((↑b.repr : M →ₗ[R] ι →₀ R) ∘ₗ Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) :
      (a : (↑w : Type v) →₀ R) → ι →₀ R)
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
fapply card_le_of_surjective' R

Premises used: card_le_of_surjective'
-- 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 : 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) ⊤
⊢ Finsupp.{v, u} (↑w : Type v) R →ₗ[R] ι →₀ R

Tactic:
exact b.repr.toLinearMap.comp (Finsupp.linearCombination R (↑))

Premises used: Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, 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 : 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) ⊤
i : Surjective (α := M) (β := ι →₀ R) (⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R)
i₁ :
  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)
⊢ Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := ι →₀ R)
    (⇑((↑b.repr : M →ₗ[R] ι →₀ R) ∘ₗ Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) :
      (a : (↑w : Type v) →₀ R) → ι →₀ R)

Tactic:
apply Surjective.comp (g := b.repr.toLinearMap)

Premises used: Function.Surjective.comp
-- 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 : 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 (α := M) (β := ι →₀ R) (⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R)

Tactic:
apply LinearEquiv.surjective

Premises used: LinearEquiv.surjective
-- 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 : 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) ⊤
i : Eq.{v + 1} (α := Submodule R M) (span R (range (ι := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ 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)

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

Premises used: LinearMap.range_eq_top, Finsupp.range_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 : 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) ⊤
⊢ Eq.{v + 1} (α := Submodule R M) (span R (range (ι := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w)))) ⊤

Tactic:
simpa using 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 : 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) ⊤
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
-- 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 : 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
⊢ Finite ι

Tactic:
haveI := basis_finite_of_finite_spans w.toFinite s b
-- 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 : 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 ι
intro : ∀ (val : Fintype ι), #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_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 : 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 ι
intro :
  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 : 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 ι
intro : 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 : 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 ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
Basis.le_span'' b s

Premises used: Basis.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 : 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 ι ≤ Fintype.card.{v} (↑w : Type v)

Tactic:
exact Basis.le_span'' b s

Premises used: Basis.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
ι : Type w
inst_3 : RankCondition R
J : Set M
v : Basis ι R M
hJ : Eq (α := Submodule R M) (span R J) ⊤
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
-- 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
inl : ∀ (val : Fintype (↑J : Type v)), #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)
inr : Infinite.{v + 1} (↑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)

Tactic:
cases fintypeOrInfinite J

Premises used: Set.Elem, fintypeOrInfinite
-- 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 : Fintype (↑J : Type v)
inl : lift.{v, w} #ι ≤ lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v})
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)

Tactic:
rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]

Premises used: Cardinal.mk_range_eq_of_injective, Set.Elem, Module.Basis.injective, Cardinal.mk_fintype, Cardinal.lift_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
ι : 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.{v, w} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{w})

Tactic:
Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)

Premises used: Iff.mpr, basis_le_span', Cardinal.lift_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
ι : 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)
h :
  lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v}) =
    lift.{v, w} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{w})
⊢ lift.{v, w} #ι ≤ lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v})

Tactic:
convert! Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
-- 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 : Fintype (↑J : Type v)
⊢ lift.{w, v} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{v}) =
    lift.{v, w} (↑(Fintype.card.{v} (↑J : Type v)) : Cardinal.{w})

Tactic:
simp
-- 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
rcases : ∀ (i : ι) (hi : (v : (a : ι) → M) i = b), Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b

Tactic:
rcases mem_range.1 hb with ⟨i, hi⟩

Premises used: Set.mem_range, Iff.mp
-- 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
b : M
hb : Membership.mem (γ := Set M) (range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) b
i : ι
hi : (v : (a : ι) → M) i = b
⊢ 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⟩
-- 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_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))
⊢ ⊤ ≤ comap (↑v.repr : M →ₗ[R] ι →₀ R) (Finsupp.supported R R (⋃ (j : (↑J : Type v)), S j))

Tactic:
rw [hJ] at this
-- 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_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 (α := ι →₀ 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
-- 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_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)
⊢ (↑{i} : Set ι) ⊆ ⋃ (j : (↑J : Type v)), S j

Tactic:
rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this

Premises used: Finsupp.support_single, Finsupp.mem_supported, one_ne_zero, Module.Basis.repr_self
-- 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_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
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)
⊢ Membership.mem (γ := Set M) (⋃ (j : (↑J : Type v)), S' j) b

Tactic:
subst b
-- 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_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)
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)
⊢ 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⟩

Premises used: Finset.mem_singleton_self, Set.mem_iUnion, Iff.mp
-- 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_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)
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:
mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion, Set.mem_image, And.intro, Exists.intro, rfl
-- 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_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)
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:
exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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
⊢ 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⟩⟩
-- 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)
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)

Tactic:
le_of_not_gt fun IJ => ?_

Premises used: le_of_not_gt
-- 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)
inr : ∀ (IJ : #(↑J : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)), False
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) ≤ #(↑J : Type v)

Tactic:
refine le_of_not_gt fun IJ => ?_

Premises used: le_of_not_gt
-- 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_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
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)
this : #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ False

Tactic:
not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩

Premises used: Nonempty.intro, not_le_of_gt, Set.embeddingOfSubset
-- 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_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
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)
this : #(↑(⋃ (j : (↑J : Type v)), S' j) : Type v) < #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ False

Tactic:
exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩

Premises used: Nonempty.intro, not_le_of_gt, Set.embeddingOfSubset