awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
s : { s : Set M // LinearIndepOn R id s }
succ :
  ∀ (le : (↑n : Cardinal.{v}) < #(↑(↑s : Set M) : Type v)),
    ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
⊢ #(↑(↑s : Set M) : Type v) ≤ (↑n : Cardinal.{v})

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 : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑n : Cardinal.{v}) < #(↑(↑s : Set M) : Type v)
⊢ (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)

Tactic:
rw [← natCast_add_one_le_iff, ← Nat.cast_add_one] at le

Premises used: Cardinal.natCast_add_one_le_iff, Nat.cast_add_one
-- 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 : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
succ :
  ∀ (t : Finset (↑(↑s : Set M) : Type v)) (ht : n + 1 = t.card),
    ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
have ⟨t, ht⟩ := exists_finset_eq_card 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 : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
t : Finset (↑(↑s : Set M) : Type v)
ht : n + 1 = t.card
⊢ (Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ (↑s : Set M)) t).card = n + 1

Tactic:
simpa using ht.symm

Premises used: Eq.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
inst_3 : Nontrivial R
n : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
t : Finset (↑(↑s : Set M) : Type v)
ht : n + 1 = t.card
⊢ (↑(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ (↑s : Set M)) t) : Set M) ⊆ (↑s : Set M)

Tactic:
simp
-- 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 : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
t : Finset (↑(↑s : Set M) : Type v)
ht : n + 1 = t.card
⊢ ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
exact ⟨t.map (.subtype _), by simpa using ht.symm, s.2.mono <| by simp⟩
-- 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 : ℕ
h : ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
s : Finset M
card_s : s.card = n
ind_s : LinearIndepOn R id (↑s : Set M)
⊢ #(↑(↑s : Set M) : Type v) = (↑n : Cardinal.{v})

Tactic:
simpa using card_s
-- 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 : ℕ
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔ ∃ (v : Fin n → M), LinearIndependent R v

Tactic:
le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩

Premises used: Exists, Module.le_rank_iff_exists_finset, id, And, SetLike.coe, LinearIndependent, Iff.intro, Finset.card, Iff.trans, _private.0.Module.le_rank_iff_exists_finset.match_1, Eq, LinearIndepOn, _private.0.Module.le_rank_iff.match_1
-- 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 : ℕ
refine_1 :
  (∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)) →
    ∀ (s : Finset M) (s_card : s.card = n) (s_ind : LinearIndepOn R id (↑s : Set M)),
      ∃ (v : Fin n → M), LinearIndependent R v
refine_2 :
  (∃ (v : Fin n → M), LinearIndependent R v) →
    ∀ (v : Fin n → M) (v_ind : LinearIndependent R v), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔ ∃ (v : Fin n → M), LinearIndependent R v

Tactic:
refine le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩

Premises used: Module.le_rank_iff_exists_finset, Iff.intro, Iff.trans
-- 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 : ℕ
h : ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
s : Finset M
s_card : s.card = n
s_ind : LinearIndepOn R id (↑s : Set M)
⊢ ∃ (v : Fin n → M), LinearIndependent R v

Tactic:
⟨_, s_ind.comp _ (s.equivFinOfCardEq s_card).symm.injective⟩

Premises used: Finset.equivFinOfCardEq, Exists.intro, Equiv.injective, Equiv.symm, LinearIndependent.comp
-- 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 : ℕ
h : ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
s : Finset M
s_card : s.card = n
s_ind : LinearIndepOn R id (↑s : Set M)
⊢ ∃ (v : Fin n → M), LinearIndependent R v

Tactic:
exact ⟨_, s_ind.comp _ (s.equivFinOfCardEq s_card).symm.injective⟩
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ (Finset.map { toFun := v, inj' := ⋯ : Fin n ↪ M } Finset.univ).card = n

Tactic:
simp
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
refine_2 : LinearIndepOn R id (↑(Finset.map { toFun := v, inj' := ⋯ : Fin n ↪ M } Finset.univ) : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
refine ⟨.map ⟨_, v_ind.injective⟩ .univ, by simp, ?_⟩
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ LinearIndepOn R id (↑(Finset.map { toFun := v, inj' := ⋯ : Fin n ↪ M } Finset.univ) : Set M)

Tactic:
simpa using (linearIndepOn_id_range_iff v_ind.injective).mpr v_ind

Premises used: Iff.mpr, linearIndepOn_id_range_iff, LinearIndependent.injective
-- 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 : ℕ
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔
    ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)

Tactic:
le_rank_iff.trans ⟨fun ⟨v, v_ind⟩ ↦ ?_, fun ⟨f, f_inj⟩ ↦
    ⟨_, (Module.Basis.ofEquivFun <| .refl ..).linearIndependent.map_injOn f f_inj.injOn⟩⟩

Premises used: Module.Basis.ofEquivFun, Function.Injective.injOn, Module.le_rank_iff, Function.comp, Exists, LinearIndependent.map_injOn, Module.Basis.linearIndependent, LinearIndependent, Iff.intro, Exists.intro, Iff.trans, LinearEquiv.refl, Function.Injective, _private.0.Module.le_rank_iff_exists_linearMap.match_1, DFunLike.coe, _private.0.Module.le_rank_iff.match_1
-- 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 : ℕ
refine :
  (∃ (v : Fin n → M), LinearIndependent R v) →
    ∀ (v : Fin n → M) (v_ind : LinearIndependent R v),
      ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔
    ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)

Tactic:
refine le_rank_iff.trans ⟨fun ⟨v, v_ind⟩ ↦ ?_, fun ⟨f, f_inj⟩ ↦
    ⟨_, (Module.Basis.ofEquivFun <| .refl ..).linearIndependent.map_injOn f f_inj.injOn⟩⟩

Premises used: Module.le_rank_iff, Iff.intro, Iff.trans
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ Injective.{max 1 (u + 1), v + 1} (α := Fin n → R) (β := M)
    (comp (β := Fin n →₀ R) (⇑(Finsupp.linearCombination R v) : (a : Fin n →₀ R) → M)
      (⇑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R (Fin n))) : (a : Fin n → R) → Fin n →₀ R))

Tactic:
have := Injective.comp v_ind (Finsupp.linearEquivFunOnFinite R ..).symm.injective
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
this :
  Injective.{max 1 (u + 1), v + 1} (α := Fin n → R) (β := M)
    (comp (β := Fin n →₀ R) (⇑(Finsupp.linearCombination R v) : (a : Fin n →₀ R) → M)
      (⇑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R (Fin n))) : (a : Fin n → R) → Fin n →₀ R))
⊢ ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)

Tactic:
⟨Finsupp.linearCombination .. ∘ₗ _, this⟩

Premises used: LinearMap.comp, Exists.intro, Finsupp.linearCombination
-- 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 : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
this :
  Injective.{max 1 (u + 1), v + 1} (α := Fin n → R) (β := M)
    (comp (β := Fin n →₀ R) (⇑(Finsupp.linearCombination R v) : (a : Fin n →₀ R) → M)
      (⇑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R (Fin n))) : (a : Fin n → R) → Fin n →₀ R))
⊢ ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)

Tactic:
exact ⟨Finsupp.linearCombination .. ∘ₗ _, this⟩
-- 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 : Subsingleton R
h₁ : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ 1
h₂ : ∀ w < 1, ∃ (i : { s : Set M // LinearIndepOn R id s }), w < #(↑(↑i : Set M) : Type v)
⊢ Module.rank R M = 1

Tactic:
rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]

Premises used: Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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 : Subsingleton R
⊢ Subsingleton M

Tactic:
have := Module.subsingleton R M
-- 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 : Subsingleton R
this : Subsingleton M
⊢ ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ 1

Tactic:
simp [Set.subsingleton_of_subsingleton]

Premises used: Set.subsingleton_of_subsingleton
-- 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 : Subsingleton R
w : Cardinal.{v}
hw : w < 1
⊢ ∃ (i : { s : Set M // LinearIndepOn R id s }), w < #(↑(↑i : Set M) : Type v)

Tactic:
⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

Premises used: LinearIndepOn.of_subsingleton, LT.lt.trans_eq, Subtype.mk, Exists.intro, Cardinal.mk_singleton, Singleton.singleton, OfNat.ofNat, Eq.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
inst_3 : Subsingleton R
w : Cardinal.{v}
hw : w < 1
⊢ ∃ (i : { s : Set M // LinearIndepOn R id s }), w < #(↑(↑i : Set M) : Type v)

Tactic:
exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
⊢ 1 ≤ Module.rank R M ↔ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)

Tactic:
le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩

Premises used: _private.0.Module.one_le_rank_iff.match_2, Module.le_rank_iff_exists_linearMap, Exists, _private.0.Module.one_le_rank_iff.match_1, Iff.intro, Iff.trans, Function.Injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
refine_1 :
  (∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)) →
    ∀ (f : (Fin 1 → R) →ₗ[R] M) (hf : Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)),
      ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
refine_2 :
  (∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)) →
    ∀ (f : R →ₗ[R] M) (hf : Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)),
      ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
⊢ 1 ≤ Module.rank R M ↔ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)

Tactic:
refine le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩

Premises used: Module.le_rank_iff_exists_linearMap, Iff.intro, Iff.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
h_1 : ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
f : (Fin 1 → R) →ₗ[R] M
hf : Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
⊢ Injective.{u + 1, v + 1} (α := R) (β := M)
    (⇑(f ∘ₗ (↑(LinearEquiv.symm (LinearEquiv.piUnique R fun (a : Fin 1) ↦ R)) : R →ₗ[R] (t : Fin 1) → R)) : (a : R) → M)

Tactic:
apply hf.comp (LinearEquiv.piUnique R ..).symm.injective

Premises used: LinearEquiv.symm, Function.Injective.comp, LinearEquiv.piUnique, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
h_1 : ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
f : (Fin 1 → R) →ₗ[R] M
hf : Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
⊢ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)

Tactic:
exact ⟨f ∘ₗ _, by apply hf.comp (LinearEquiv.piUnique R ..).symm.injective⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
h_1 : ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
f : R →ₗ[R] M
hf : Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
⊢ ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)

Tactic:
⟨f ∘ₗ _, hf.comp (LinearEquiv.piUnique R ..).injective⟩

Premises used: LinearMap.comp, Function.Injective.comp, Exists.intro, LinearEquiv.piUnique, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
h_1 : ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
f : R →ₗ[R] M
hf : Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
⊢ ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)

Tactic:
exact ⟨f ∘ₗ _, hf.comp (LinearEquiv.piUnique R ..).injective⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
simp_rw :
  LE.le (α := Cardinal.{max v v'})
    (⨆ (i : { s : Set M // LinearIndepOn R id s }), lift.{v', v} #(↑(↑i : Set M) : Type v))
    (⨆ (i : { s : Set M' // LinearIndepOn R' id s }), lift.{v, v'} #(↑(↑i : Set M') : Type v'))
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small, Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ LE.le (α := Cardinal.{max v v'})
    (⨆ (i : { s : Set M // LinearIndepOn R id s }), lift.{v', v} #(↑(↑i : Set M) : Type v))
    (⨆ (i : { s : Set M' // LinearIndepOn R' id s }), lift.{v, v'} #(↑(↑i : Set M') : Type v'))

Tactic:
ciSup_mono_of_forall_exists' bddAbove_of_small fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
    LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

Premises used: Iff.mpr, _private.0.lift_rank_le_of_injective_injectiveₛ.match_1, LinearIndependent.map_of_injective_injectiveₛ, LinearIndepOn.linearIndependent, Equiv.Set.image, Cardinal.lift, Cardinal.mk, Exists, Set.Elem, LE.le, Nonempty.intro, Subtype.mk, Equiv.toEmbedding, Exists.intro, Cardinal.lift_mk_le', ciSup_mono_of_forall_exists', Set.image, Cardinal.bddAbove_of_small, LinearIndepOn.id_image, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ LE.le (α := Cardinal.{max v v'})
    (⨆ (i : { s : Set M // LinearIndepOn R id s }), lift.{v', v} #(↑(↑i : Set M) : Type v))
    (⨆ (i : { s : Set M' // LinearIndepOn R' id s }), lift.{v, v'} #(↑(↑i : Set M') : Type v'))

Tactic:
exact ciSup_mono_of_forall_exists' bddAbove_of_small fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
    LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

Premises used: ciSup_mono_of_forall_exists', Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
obtain : ∀ (i' : R' → R) (hi' : RightInverse i' i), lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
obtain ⟨i', hi'⟩ := hi.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_

Premises used: lift_rank_le_of_injective_injectiveₛ
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
refine_1 : ∀ (x x_1 : R') (h : i' x = i' x_1), x = x_1
refine_2 : ∀ (r : R') (m : M), (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_

Premises used: lift_rank_le_of_injective_injectiveₛ
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i' x = i' x_1
⊢ i (i' x) = i (i' x_1)

Tactic:
apply_fun i at h
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i (i' x) = i (i' x_1)
refine_1 : ∀ (h : x = i (i' x_1)), x = x_1
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (h : x = x_1), x = x_1
⊢ x = x_1

Tactic:
rwa [hi', hi'] at h
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
refine_2 :
  HSMul.hSMul (β := M') (i (i' r)) ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
refine_2₁ refine_2₂ :
  HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')

Tactic:
rw [hc (i' r) m, hi']