awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h_1 :
  ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑g : (a : ℕ →₀ R) → Fin n → R)
h : Module.rank R (Fin n → R) = Cardinal.lift.{0, u} (Module.rank R (Fin n → R))
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
convert! (Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, Function.Injective.injOn, Finsupp.basisSingleOne, LinearIndependent.map_injOn, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h :
  ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑g : (a : ℕ →₀ R) → Fin n → R)
⊢ Module.rank R (Fin n → R) = Cardinal.lift.{0, u} (Module.rank R (Fin n → R))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
rw : (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)
⊢ StrongRankCondition R ↔ ∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
rw [strongRankCondition_iff_forall_rank_lt_aleph0, ← not_iff_not]

Premises used: not_iff_not, strongRankCondition_iff_forall_rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
push : (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
simp_rw :
  (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0

Tactic:
simp_rw [finrank, Nat.le_zero, toNat_eq_zero]

Premises used: Nat.le_zero, Cardinal.toNat_eq_zero, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩

Premises used: _private.0.strongRankCondition_iff_forall_rank_lt_aleph0.match_2, Exists, Cardinal.aleph0, LE.le, GT.gt, And, HAdd.hAdd, Nat.succ_pos, And.intro, Iff.intro, Exists.intro, Or, Module.rank, OfNat.ofNat, Eq, _private.0.strongRankCondition_iff_forall_zero_lt_finrank.match_2
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
refine_1 :
  (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) →
    ∀ (n : ℕ) (le : ℵ₀ ≤ Module.rank R (Fin n → R)),
      Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)
refine_2 :
  (∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)) →
    ∀ (n : ℕ) (pos : n > 0) (eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)),
      ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
refine ⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
le : ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)

Tactic:
.inr <| le.trans <| LinearMap.rank_le_of_injective
      (ExtendByZero.linearMap R _) <| extend_injective (Fin.castSucc_injective n) _

Premises used: Function.extend_injective, Fin.castSucc_injective, LinearMap.rank_le_of_injective, Function.ExtendByZero.linearMap, LE.le.trans, Or.inr
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
le : ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)

Tactic:
exact .inr <| le.trans <| LinearMap.rank_le_of_injective
      (ExtendByZero.linearMap R _) <| extend_injective (Fin.castSucc_injective n) _

Premises used: Function.extend_injective, Fin.castSucc_injective, LinearMap.rank_le_of_injective, Function.ExtendByZero.linearMap, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ (∃ (f : R →ₗ[R] Fin n → R), Injective (α := R) (β := Fin n → R) (⇑f : (a : R) → Fin n → R)) →
    ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
rw [or_iff_not_imp_left, ← Ne, ← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at eq

Premises used: Module.one_le_rank_iff, Cardinal.one_le_iff_ne_zero, Ne, Classical.or_iff_not_imp_left
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq :
  (∃ (f : R →ₗ[R] Fin n → R), Injective (α := R) (β := Fin n → R) (⇑f : (a : R) → Fin n → R)) →
    ℵ₀ ≤ Module.rank R (Fin n → R)
refine_2 :
  ∀
    (eq :
      (∃ (f : R →ₗ[R] Fin n.pred.succ → R),
          Injective (α := R) (β := Fin n.pred.succ → R) (⇑f : (a : R) → Fin n.pred.succ → R)) →
        ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)),
    ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
rw [← n.succ_pred_eq_of_pos pos] at eq ⊢

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq :
  (∃ (f : R →ₗ[R] Fin n.pred.succ → R),
      Injective (α := R) (β := Fin n.pred.succ → R) (⇑f : (a : R) → Fin n.pred.succ → R)) →
    ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)

Tactic:
eq ⟨.single R (fun _ ↦ _) 0, Pi.single_injective (M := fun _ ↦ _) _⟩

Premises used: LinearMap.single, Pi.single_injective, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq :
  (∃ (f : R →ₗ[R] Fin n.pred.succ → R),
      Injective (α := R) (β := Fin n.pred.succ → R) (⇑f : (a : R) → Fin n.pred.succ → R)) →
    ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)

Tactic:
exact eq ⟨.single R (fun _ ↦ _) 0, Pi.single_injective (M := fun _ ↦ _) _⟩

Premises used: LinearMap.single, Pi.single_injective, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : ∀ (n : ℕ), IsNoetherian R (Fin n → R)
⊢ StrongRankCondition R

Tactic:
(strongRankCondition_iff_succ R).2 fun n f hf ↦
    have e := LinearEquiv.piCongrLeft R (fun _ ↦ R) (finSuccEquiv n) ≪≫ₗ .piOptionEquivProd _
    not_subsingleton R <| IsNoetherian.subsingleton_of_injective
      (f := f ∘ₗ e.symm.toLinearMap) (hf.comp e.symm.injective)

Premises used: Iff.mpr, LinearEquiv.symm, IsNoetherian.subsingleton_of_injective, LinearEquiv.piCongrLeft, finSuccEquiv, Function.Injective.comp, LinearEquiv.piOptionEquivProd, not_subsingleton, LinearEquiv.injective, LinearEquiv.trans, strongRankCondition_iff_succ
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
rcases :
  ∀ (t : Set M) (ht_sub : t ⊆ s) (ht_span : Eq (α := Submodule K M) (span K t) (span K s))
    (ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))),
    ∃ (t : Finset M),
      (↑t : Set M) ⊆ s ∧
        t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
          Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)

Tactic:
rcases exists_linearIndependent K s with ⟨t, ht_sub, ht_span, ht_indep⟩

Premises used: exists_linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
rw : #(↑t : Type u_3) = (↑(finrank.{u_2, u_3} K ↥(span K s)) : Cardinal.{u_3})
rw₁ : #(↑t : Type u_3) = Module.rank K ↥(span K s)
rw₂ : #(↑t : Type u_3) = Module.rank K ↥(span K t)
rw₃ rw₄ : #(↑t : Type u_3) = #(↑t : Type u_3)
⊢ ∃ (u : Finset M), (↑u : Set M) = t ∧ u.card = finrank.{u_2, u_3} K ↥(span K s)

Tactic:
rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]

Premises used: rank_span_set, Module.finrank_eq_rank, Cardinal.mk_set_eq_nat_iff_finset
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
obtain :
  ∀ (t : Finset M) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)) (ht_sub : (↑t : Set M) ⊆ s)
    (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s))
    (ht_indep :
      LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ (↑t : Set M) }) K
        (Subtype.val (p := fun (x : M) ↦ x ∈ (↑t : Set M)))),
    ∃ (t : Finset M),
      (↑t : Set M) ⊆ s ∧
        t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
          Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)

Tactic:
obtain ⟨t, rfl, ht_card⟩ : ∃ u : Finset M, ↑u = t ∧ u.card = finrank K (span K s) := by
    rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]

Premises used: Finset, Membership.mem, Subtype, Submodule.span, Module.finrank, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Finset M
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_sub : (↑t : Set M) ⊆ s
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep :
  LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ (↑t : Set M) }) K
    (Subtype.val (p := fun (x : M) ↦ x ∈ (↑t : Set M)))
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)

Tactic:
⟨t, ht_sub, ht_card, ht_span, ht_indep⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Finset M
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_sub : (↑t : Set M) ⊆ s
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep :
  LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ (↑t : Set M) }) K
    (Subtype.val (p := fun (x : M) ↦ x ∈ (↑t : Set M)))
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)

Tactic:
exact ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
rcases :
  ∀ (t : Finset M) (hts : (↑t : Set M) ⊆ s) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s))
    (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)) (ht_indep : LinearIndepOn K id (↑t : Set M)),
    ∃ (f : Fin (finrank.{u_2, u_3} K ↥(span K s)) → M),
      (∀ (i : Fin (finrank.{u_2, u_3} K ↥(span K s))), f i ∈ s) ∧
        Eq (α := Submodule K M) (span K (range f)) (span K s) ∧ LinearIndependent K f
⊢ ∃ (f : Fin (finrank.{u_2, u_3} K ↥(span K s)) → M),
    (∀ (i : Fin (finrank.{u_2, u_3} K ↥(span K s))), f i ∈ s) ∧
      Eq (α := Submodule K M) (span K (range f)) (span K s) ∧ LinearIndependent K f

Tactic:
rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩

Premises used: Submodule.exists_finset_span_eq_linearIndepOn
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Finset M
hts : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
e : Fin (finrank.{u_2, u_3} K ↥(span K s)) ≃ ↥t := (Finset.equivFinOfCardEq ht_card).symm
⊢ Eq (α := Submodule K M)
    (span K
      (range (ι := Fin (finrank.{u_2, u_3} K ↥(span K s)))
        (comp (β := ↥t) (Subtype.val (p := fun (x : M) ↦ x ∈ t)) (⇑e : (a : Fin (finrank K ↥(span K s))) → ↥t))))
    (span K s)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Finset M
hts : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
e : Fin (finrank.{u_2, u_3} K ↥(span K s)) ≃ ↥t := (Finset.equivFinOfCardEq ht_card).symm
⊢ ∃ (f : Fin (finrank.{u_2, u_3} K ↥(span K s)) → M),
    (∀ (i : Fin (finrank.{u_2, u_3} K ↥(span K s))), f i ∈ s) ∧
      Eq (α := Submodule K M) (span K (range f)) (span K s) ∧ LinearIndependent K f

Tactic:
exact ⟨(↑) ∘ e, fun i ↦ hts (e i).2, by simpa, ht_indep.comp _ e.injective⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
mp :
  Membership.mem (γ := Submodule K M) (span K s) x →
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
mpr :
  (∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x) →
    Membership.mem (γ := Submodule K M) (span K s) x
⊢ Membership.mem (γ := Submodule K M) (span K s) x ↔
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
mp :
  ∀ (t : Finset M) (ht_sub : (↑t : Set M) ⊆ s) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s))
    (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)) (ht_indep : LinearIndepOn K id (↑t : Set M)),
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x

Tactic:
rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩

Premises used: Submodule.exists_finset_span_eq_linearIndepOn
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
mp :
  ∀ (c : M →₀ K) (hct : (↑c.support : Set M) ⊆ (↑t : Set M)) (hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x),
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x

Tactic:
rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩

Premises used: Submodule.mem_span_set, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
c : M →₀ K
hct : (↑c.support : Set M) ⊆ (↑t : Set M)
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x

Tactic:
⟨c, ?_, hct.trans ht_sub, hx⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
c : M →₀ K
hct : (↑c.support : Set M) ⊆ (↑t : Set M)
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
mp : c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s)
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x

Tactic:
refine ⟨c, ?_, hct.trans ht_sub, hx⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
c : M →₀ K
hct : (↑c.support : Set M) ⊆ (↑t : Set M)
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s)

Tactic:
ht_card ▸ Finset.card_mono hct

Premises used: Eq.rec, Finset.card_mono
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
c : M →₀ K
hct : (↑c.support : Set M) ⊆ (↑t : Set M)
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s)

Tactic:
exact ht_card ▸ Finset.card_mono hct
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
c : M →₀ K
hcs : (↑c.support : Set M) ⊆ s
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ Membership.mem (γ := Submodule K M) (span K s) x

Tactic:
mem_span_set.mpr ⟨c, hcs, hx⟩

Premises used: Iff.mpr, Submodule.mem_span_set, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
c : M →₀ K
hcs : (↑c.support : Set M) ⊆ s
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ Membership.mem (γ := Submodule K M) (span K s) x

Tactic:
exact mem_span_set.mpr ⟨c, hcs, hx⟩

Premises used: Iff.mpr, Submodule.mem_span_set, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : StrongRankCondition R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : IsQuadraticExtension R S
⊢ finrank R S = 2

Tactic:
finrank_eq_two'

Premises used: Algebra.IsQuadraticExtension.finrank_eq_two'
-- Module: Mathlib.LinearAlgebra.Dimension.Subsingleton
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
rw :
  LE.le.{u_2 + 1} (α := Cardinal.{u_2})
    (⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2)) ⊥
⊢ Module.rank R M = 0

Tactic:
rw [Module.rank, ← bot_eq_zero, eq_bot_iff]

Premises used: Module.rank, eq_bot_iff, bot_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Subsingleton
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
s : { s : Set M // LinearIndepOn R id s }
⊢ Cardinal.mk (↑(↑s : Set M) : Type u_2) ≤ ⊥

Tactic:
simp [(linearIndependent_subsingleton_iff _).mp s.2]

Premises used: Iff.mp, linearIndependent_subsingleton_iff, Subtype.property
-- Module: Mathlib.LinearAlgebra.Dimension.Subsingleton
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2})
    (⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2)) ⊥

Tactic:
exact ciSup_le fun s ↦ by simp [(linearIndependent_subsingleton_iff _).mp s.2]

Premises used: ciSup_le