awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
simp_rw :
  Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R))
    (∑ k : ι',
      (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) k : R)
            ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) k) : ι →₀ R) :
          (a : ι) → R)
        i)
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
        HMul.hMul (α := R) (β := R)
          ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
      R)
    (((b.repr : (a : M) → ι →₀ R)
            (∑ i : ι',
              HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
                ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
          (a : ι) → R)
        i :
      R)

Tactic:
simp_rw [map_sum, map_smul, Finset.sum_apply']

Premises used: Finset.sum_apply', map_sum, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R))
    (∑ k : ι',
      (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) k : R)
            ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) k) : ι →₀ R) :
          (a : ι) → R)
        i)

Tactic:
Finset.sum_congr rfl fun j _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
refine :
  ∀ (j : ι'),
    Membership.mem (γ := Finset ι') Finset.univ j →
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
        (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
              ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
            (a : ι) → R)
          i
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R))
    (∑ k : ι',
      (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) k : R)
            ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) k) : ι →₀ R) :
          (a : ι) → R)
        i)

Tactic:
refine Finset.sum_congr rfl fun j _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
h : Membership.mem (γ := Finset ι') Finset.univ j
rw :
  HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    HSMul.hSMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
rw₂ rw₃ :
  HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R) =
    HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
⊢ HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
          ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
        (a : ι) → R)
      i

Tactic:
rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

Premises used: Finsupp.smul_apply, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x : M
⊢ (∀ (i : ι), Eq.{u_11 + 1} (α := R) ((b.coord i : (a : M) → R) x : R) (0 : R)) ↔
    Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) (0 : ι →₀ R)

Tactic:
simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply]

Premises used: DFunLike.ext_iff, Finsupp.zero_apply, Module.Basis.coord_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
⊢ Eq (α := (a : M) → R) (⇑b.sumCoords : (a : M) → R) fun (m : M) ↦
    sum (M := R) ((b.repr : (a : M) → ι →₀ R) m) fun (x : ι) ↦ id

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
h : ∀ (m : M), Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) ((∑ i : ι, b.coord i : (a : M) → R) m : R)
⊢ Eq (α := (a : M) → R) (⇑b.sumCoords : (a : M) → R) (⇑(∑ i : ι, b.coord i) : (a : M) → R)

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
m : M
⊢ Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) ((∑ i : ι, b.coord i : (a : M) → R) m : R)

Tactic:
simp only [sumCoords, Finsupp.sum_fintype, LinearMap.id_coe, LinearEquiv.coe_coe, coord_apply,
    id, Fintype.sum_apply, imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, comp_apply,
    LinearMap.coe_sum]

Premises used: LinearMap.id_coe, Finsupp.sum_fintype, id, LinearMap.coe_sum, Module.Basis.sumCoords, imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, Function.comp_apply, Fintype.sum_apply, Module.Basis.coord_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
⊢ Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) ((b : (a : ι) → M) i : M) : R) (1 : R)

Tactic:
simp only [Basis.sumCoords, LinearMap.id_coe, LinearEquiv.coe_coe, id, Basis.repr_self,
    Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp, Finsupp.sum_single_index]

Premises used: Finsupp.sum_single_index, LinearMap.id_coe, id, Module.Basis.sumCoords, Finsupp.coe_lsum, LinearMap.coe_comp, Function.comp_apply, Module.Basis.repr_self, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
m : M
r : R
⊢ (b.coord i : (a : M) → R) (r • m) = HMul.hMul (β := R) r ((b.coord i : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
f : ι →₀ R
⊢ Eq.{u_11 + 1} (α := R) ((b.coord i : (a : M) → R) ((b.repr.symm : (a : ι →₀ R) → M) f : M) : R)
    ((f : (a : ι) → R) i : R)

Tactic:
simp only [repr_symm_apply, coord_apply, repr_linearCombination]

Premises used: Module.Basis.repr_linearCombination, Module.Basis.repr_symm_apply, Module.Basis.coord_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
h : ∀ (m : M), Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) (∑ᶠ (i : ι), (b.coord i : (a : M) → R) m : R)
⊢ Eq (α := (a : M) → R) (⇑b.sumCoords : (a : M) → R) fun (m : M) ↦ ∑ᶠ (i : ι), (b.coord i : (a : M) → R) m

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
m : M
⊢ Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) (∑ᶠ (i : ι), (b.coord i : (a : M) → R) m : R)

Tactic:
simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe,
    LinearEquiv.coe_coe, Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp,
    finsum_eq_sum _ (b.repr m).hasFiniteSupport, Finsupp.sum, Finset.finite_toSet_toFinset, id,
    Finsupp.fun_support_eq]

Premises used: Module.Basis.coord, Finsupp.fun_support_eq, LinearMap.id_coe, finsum_eq_sum, Finset.finite_toSet_toFinset, Finsupp.sum, id, Module.Basis.repr, Module.Basis.sumCoords, Finsupp.coe_lsum, Finsupp.lapply_apply, LinearMap.coe_comp, Finsupp.hasFiniteSupport, Function.comp_apply, DFunLike.coe, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
h :
  ∀ (x : M), Eq.{u_11 + 1} (α := R) (((b.reindex e).sumCoords : (a : M) → R) x : R) ((b.sumCoords : (a : M) → R) x : R)
⊢ (b.reindex e).sumCoords = b.sumCoords

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
h :
  Eq.{u_11 + 1} (α := R)
    (sum (M := R) (mapDomain.{u_10, u_2, u_11} (α := ι) (⇑e : (a : ι) → ι') ((b.repr : (a : M) → ι →₀ R) x))
      fun (x : ι') ↦ id)
    (sum (M := R) ((b.repr : (a : M) → ι →₀ R) x) fun (x : ι) ↦ id)
⊢ Eq.{u_11 + 1} (α := R) (((b.reindex e).sumCoords : (a : M) → R) x : R) ((b.sumCoords : (a : M) → R) x : R)

Tactic:
simp only [coe_sumCoords, repr_reindex]

Premises used: Module.Basis.repr_reindex, Module.Basis.coe_sumCoords
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ Eq.{u_11 + 1} (α := R)
    (sum (M := R) (mapDomain.{u_10, u_2, u_11} (α := ι) (⇑e : (a : ι) → ι') ((b.repr : (a : M) → ι →₀ R) x))
      fun (x : ι') ↦ id)
    (sum (M := R) ((b.repr : (a : M) → ι →₀ R) x) fun (x : ι) ↦ id)

Tactic:
Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

Premises used: Finsupp.sum_mapDomain_index, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ Eq.{u_11 + 1} (α := R)
    (sum (M := R) (mapDomain.{u_10, u_2, u_11} (α := ι) (⇑e : (a : ι) → ι') ((b.repr : (a : M) → ι →₀ R) x))
      fun (x : ι') ↦ id)
    (sum (M := R) ((b.repr : (a : M) → ι →₀ R) x) fun (x : ι) ↦ id)

Tactic:
exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

Premises used: Finsupp.sum_mapDomain_index
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
i : ι
f : ι → R
⊢ (b.coord i : (a : M) → R) ((b.equivFun.symm : (a : ι → R) → M) f : M) = f i

Tactic:
b.coord_repr_symm i (Finsupp.equivFunOnFinite.symm f)

Premises used: Finsupp.equivFunOnFinite, Equiv.symm, DFunLike.coe, Module.Basis.coord_repr_symm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Module.rank R M ≤ #M

Tactic:
(Module.rank_def _ _).trans_le (ciSup_le' fun _ ↦ mk_set_le _)

Premises used: Module.rank_def, ciSup_le', Eq.trans_le, Cardinal.mk_set_le, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M M₁ : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Nonempty.{max 1 (v + 1)} { s : Set M // LinearIndepOn R id s }

Tactic:
⟨⟨∅, linearIndepOn_empty _ _⟩⟩

Premises used: Nonempty.intro, Subtype.mk, linearIndepOn_empty, EmptyCollection.emptyCollection
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
rw : lift.{v, w} #ι ≤ lift.{w, v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
rw [Module.rank]

Premises used: Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
le_trans ?_ (lift_le.mpr <| le_ciSup bddAbove_of_small ⟨_, hv.linearIndepOn_id⟩)

Premises used: Iff.mpr, le_ciSup, Cardinal.bddAbove_of_small, le_trans, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
refine :
  lift.{v, w} #ι ≤
    lift.{w, v} #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range v) ⋯) : Set M) : Type v)
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))

Tactic:
refine le_trans ?_ (lift_le.mpr <| le_ciSup bddAbove_of_small ⟨_, hv.linearIndepOn_id⟩)

Premises used: Iff.mpr, le_ciSup, Cardinal.bddAbove_of_small, le_trans, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤
    lift.{w, v} #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range v) ⋯) : Set M) : Type v)

Tactic:
lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

Premises used: Iff.mpr, LinearIndependent.injective, Nonempty.intro, Equiv.ofInjective, Equiv.toEmbedding, Cardinal.lift_mk_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤
    lift.{w, v} #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range v) ⋯) : Set M) : Type v)

Tactic:
exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

Premises used: Iff.mpr, LinearIndependent.injective, Nonempty.intro, Equiv.ofInjective, Equiv.toEmbedding, Cardinal.lift_mk_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
inst_4 : Infinite ι
v : ι → M
hv : LinearIndependent R v
⊢ ℵ₀ ≤ Module.rank R M

Tactic:
aleph0_le_lift.mp <| (aleph0_le_lift.mpr <| aleph0_le_mk ι).trans hv.cardinal_lift_le_rank

Premises used: Iff.mpr, LinearIndependent.cardinal_lift_le_rank, Cardinal.aleph0_le_lift, Iff.mp, LE.le.trans, Cardinal.aleph0_le_mk
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M

Tactic:
simpa using hv.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Set M
hs : LinearIndependent R (M := M) fun (x : (↑s : Type v)) ↦ (↑x : M)
⊢ #(↑s : Type v) ≤ Module.rank R M

Tactic:
hs.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R M)

Tactic:
simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat hs.linearIndependent.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, LinearIndepOn.linearIndependent, OrderHom.mono
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
rcases :
  ∀ (c' : Cardinal.{v}) (hc' : c' < Module.rank R M) (hcc' : lift.{w, v} c' = lift.{v, w} c),
    ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
rcases Cardinal.lt_lift_iff.mp h with ⟨c', hc', hcc'⟩

Premises used: Cardinal.lt_lift_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ c' < ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)

Tactic:
simpa [← hcc', Module.rank_def] using h

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
rcases :
  ∀ (s : Set M) (hs : LinearIndepOn R id s)
    (h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)),
    ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
rcases exists_lt_of_lt_ciSup (by simpa [← hcc', Module.rank_def] using h) with ⟨⟨s, hs⟩, h⟩

Premises used: exists_lt_of_lt_ciSup
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h_1 : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)
rcases :
  ∀ (t : Set M) (hst : t ⊆ (↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M))
    (ht : #(↑t : Type v) = c'), ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
rcases Cardinal.le_mk_iff_exists_subset.mp h.le with ⟨t, hst, ht⟩

Premises used: Cardinal.le_mk_iff_exists_subset, LT.lt.le, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h_1 : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)
t : Set M
hst : t ⊆ (↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M)
ht : #(↑t : Type v) = c'
⊢ lift.{w, v} #(↑t : Type v) = lift.{v, w} c

Tactic:
simp [ht, hcc']
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h_1 : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)
t : Set M
hst : t ⊆ (↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M)
ht : #(↑t : Type v) = c'
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
exact ⟨t, by simp [ht, hcc'], hs.mono hst⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{v}
h : c < Module.rank R M
⊢ ∃ (s : Set M), #(↑s : Type v) = c ∧ LinearIndepOn R id s

Tactic:
simpa using exists_set_linearIndependent_of_lt_lift_rank (Cardinal.lift_lt.mpr h)

Premises used: Module.exists_set_linearIndependent_of_lt_lift_rank, Iff.mpr, Cardinal.lift_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : (↑n : Cardinal.{v}) ≤ Module.rank R M
contrapose! :
  ∀ (le : ∀ (s : Finset M) (_ : s.card = n), ¬LinearIndepOn R id (↑s : Set M)), Module.rank R M < (↑n : Cardinal.{v})
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
contrapose! le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n), ¬LinearIndepOn R id (↑s : Set M)
zero :
  ∀ (le : ∀ (s : Finset M) (_ : s.card = 0), ¬LinearIndepOn R id (↑s : Set M)), Module.rank R M < (↑0 : Cardinal.{v})
succ :
  ∀ (n : ℕ) (le : ∀ (s : Finset M) (_ : s.card = n + 1), ¬LinearIndepOn R id (↑s : Set M)),
    Module.rank R M < (↑(n + 1) : Cardinal.{v})
⊢ Module.rank R M < (↑n : Cardinal.{v})

Tactic:
obtain _ | n := n
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
le : ∀ (s : Finset M) (_ : s.card = 0), ¬LinearIndepOn R id (↑s : Set M)
⊢ Module.rank R M < (↑0 : Cardinal.{v})

Tactic:
simp at le
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n + 1), ¬LinearIndepOn R id (↑s : Set M)
succ : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ (↑n : Cardinal.{v})
⊢ Module.rank R M < (↑(n + 1) : Cardinal.{v})

Tactic:
rw [Module.rank, Nat.cast_add_one, lt_natCast_add_one_iff, ciSup_le_iff bddAbove_of_small]

Premises used: ciSup_le_iff, Cardinal.bddAbove_of_small, Cardinal.lt_natCast_add_one_iff, Module.rank, Nat.cast_add_one