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 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
haveI haveI₁ haveI₂ : ∀ (this : Nontrivial R), Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})

Tactic:
classical
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

Premises used: Module.Basis.mk_range_eq_rank, 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 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
ι' : Type u_3
inst_5 : Fintype ι'
v : ι' → M
hv : LinearIndependent R v
⊢ Fintype.card ι' ≤ Fintype.card ι

Tactic:
simpa [rank_eq_card_basis b, Cardinal.mk_fintype] using hv.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, rank_eq_card_basis, 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
ι : Type w
ι' : Type w'
inst_3 : StrongRankCondition R
N : Submodule R M
inst_4 : Fintype ι
b : Basis ι R M
inst_5 : Fintype ι'
b' : Basis.{w', u, v} ι' R ↥N
⊢ Fintype.card ι' ≤ Fintype.card ι

Tactic:
b.card_le_card_of_linearIndependent
    (b'.linearIndependent.map_injOn N.subtype N.injective_subtype.injOn)

Premises used: Module.Basis.card_le_card_of_linearIndependent, Function.Injective.injOn, LinearIndependent.map_injOn, Submodule.injective_subtype, Module.Basis.linearIndependent, Submodule.subtype
-- 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
ι' : Type w'
inst_3 : StrongRankCondition R
N O : Submodule R M
hNO : N ≤ O
inst_4 : Fintype ι
b : Basis.{w, u, v} ι R ↥O
inst_5 : Fintype ι'
b' : Basis.{w', u, v} ι' R ↥N
⊢ Fintype.card ι' ≤ Fintype.card ι

Tactic:
b.card_le_card_of_linearIndependent
    (b'.linearIndependent.map_injOn (inclusion hNO) (N.inclusion_injective _).injOn)

Premises used: Module.Basis.card_le_card_of_linearIndependent, Function.Injective.injOn, LinearIndependent.map_injOn, Submodule.inclusion, Module.Basis.linearIndependent, Submodule.inclusion_injective
-- 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 : StrongRankCondition R
v : Basis ι R M
⊢ 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 : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
rw : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
rw₁ rw₂ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Tactic:
rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]

Premises used: Module.Basis.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective, Module.Basis.injective
-- 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 : StrongRankCondition R
v : Basis ι R M
⊢ Cardinal.lift.{max v m, w} #ι = Cardinal.lift.{max w m, v} (Module.rank R M)

Tactic:
Cardinal.lift_umax_eq.{w, v, m}.mpr v.mk_eq_rank

Premises used: Iff.mpr, Module.Basis.mk_eq_rank, Cardinal.lift_umax_eq
-- 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 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
⊢ 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 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
rw : Cardinal.lift.{w, v} (Module.rank R ↥(span R (range v))) = Cardinal.lift.{w, v} #(↑(range v) : Type v)
rw₁ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range v) : Type v)
rw₂ rw₃ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
⊢ Module.rank R ↥(span R (range v)) = #(↑(range v) : Type v)

Tactic:
rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]

Premises used: Module.Basis.mk_eq_rank, Cardinal.mk_range_eq_of_injective, LinearIndependent.injective, Cardinal.lift_inj, Module.Basis.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 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
rw :
  Module.rank R ↥(span R (range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s)))) =
    #(↑(range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s))) : Type v)
⊢ Module.rank R ↥(span R s) = #(↑s : Type v)

Tactic:
rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq
-- 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 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s)))) =
    #(↑(range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s))) : Type v)

Tactic:
rank_span hs

Premises used: rank_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 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s)))) =
    #(↑(range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s))) : Type v)

Tactic:
exact rank_span hs

Premises used: rank_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 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
rw :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
rw₁ :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) =
    (v '' s).encard
rw₂ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(v '' s) : Type v) : ℕ∞)
rw₃ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(range fun (x : (↑s : Type w)) ↦ v (↑x : ι)) : Type v) : ℕ∞)
rw₄ rw₅ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard

Tactic:
rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]

Premises used: LinearIndepOn.linearIndependent, Set.image_eq_range, Set.InjOn.encard_image, Set.toENat_cardinalMk, rank_span, LinearIndepOn.injOn
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R_1 : Type u
S : Type u_1
M_1 : Type v
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
ι : Type w
ι' : Type w'
inst_3 : StrongRankCondition R_1
R : Type u_3
M : Type u_4
inst_4 : Ring R
inst_5 : StrongRankCondition R
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : IsDomain R
inst_9 : Finite ι
b : Basis ι R M
P : Submodule R M → Sort u_2
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
N : Submodule R M
this : Fintype ι := Fintype.ofFinite ι
m : ℕ
hs : Fin m → ↥N
hli : LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ hs)
⊢ m ≤ Fintype.card ι

Tactic:
simpa using b.card_le_card_of_linearIndependent hli

Premises used: Module.Basis.card_le_card_of_linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
obtain : ∀ (a : ↥I) (ha : a ≠ 0), Fintype.card m = Fintype.card n
⊢ Fintype.card m = Fintype.card n

Tactic:
obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)

Premises used: Iff.mpr, Submodule.nonzero_mem_of_bot_lt, bot_lt_iff_ne_bot
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
⊢ LinearIndependent.{u_4, u_2, u_3} (ι := n) R (M := S) (⇑b : (a : n) → S)

Tactic:
have hb := b.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb : LinearIndependent.{u_4, u_2, u_3} (ι := n) R (M := S) (⇑b : (a : n) → S)
rw :
  ∀
    (hb :
      ∀ (g : n → R),
        Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0)
    (g : n → R),
    Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0 → ∀ (i : n), g i = 0
⊢ LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a

Tactic:
rw [Fintype.linearIndependent_iff] at hb ⊢

Premises used: Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0
apply : Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0
⊢ ∀ (i : n), g i = 0

Tactic:
apply hb g
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0
⊢ Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 ∨ a = 0

Tactic:
simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg

Premises used: Finset.sum_smul, smul_assoc, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 ∨ a = 0
⊢ Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0

Tactic:
hg.resolve_right ha

Premises used: Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 ∨ a = 0
⊢ Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0

Tactic:
exact hg.resolve_right ha

Premises used: Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
⊢ LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a

Tactic:
have : LinearIndependent R fun i => b i • a := by
    have hb := b.linearIndependent
    rw [Fintype.linearIndependent_iff] at hb ⊢
    intro g hg
    apply hb g
    simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
    exact hg.resolve_right ha
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
this : LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a
⊢ Fintype.card m = Fintype.card n

Tactic:
le_antisymm
    (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
      ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
    (c.card_le_card_of_linearIndependent this)

Premises used: Module.Basis.card_le_card_of_linearIndependent, LinearIndependent.map', le_antisymm, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
this : LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a
⊢ Fintype.card m = Fintype.card n

Tactic:
exact le_antisymm
    (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
      ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
    (c.card_le_card_of_linearIndependent this)

Premises used: Module.Basis.card_le_card_of_linearIndependent, LinearIndependent.map', le_antisymm, Module.Basis.linearIndependent
-- 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 : Free R M
inst_4 : Nontrivial M
⊢ 0 < Module.rank R M

Tactic:
have := Module.nontrivial R M
  (pos_of_ne_zero <| Cardinal.mk_ne_zero _).trans_le
    (Free.chooseBasis R M).linearIndependent.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, Module.nontrivial, Module.Free.ChooseBasisIndex, Module.Basis.linearIndependent, LT.lt.trans_le, pos_of_ne_zero, Cardinal.mk_ne_zero, Module.Free.chooseBasis
-- 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 : StrongRankCondition R
inst_4 : Free R M
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩

Premises used: Module.rank_pos_of_free, Iff.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
inst_3 : StrongRankCondition R
inst_4 : Free R M
refine : ∀ (h : 0 < Module.rank R M), Nontrivial M
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩
-- 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 : StrongRankCondition R
inst_4 : Free R M
h : 0 < Module.rank R M
rw : ¬Subsingleton M
⊢ Nontrivial M

Tactic:
rw [← not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- 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 : StrongRankCondition R
inst_4 : Free R M
h : 0 < Module.rank R M
h' : Subsingleton M
⊢ False

Tactic:
simp only [rank_subsingleton', lt_self_iff_false] at h

Premises used: rank_subsingleton', lt_self_iff_false
-- 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 : StrongRankCondition R
inst_4 : Free R M
rw : Module.rank R M = 0 ↔ ¬Nontrivial M
rw₁ : Nontrivial M ↔ ¬Module.rank R M = 0
rw₂ : 0 < Module.rank R M ↔ ¬Module.rank R M = 0
rw₃ rw₄ : Module.rank R M ≠ 0 ↔ ¬Module.rank R M = 0
⊢ Module.rank R M = 0 ↔ Subsingleton M

Tactic:
rw [← not_nontrivial_iff_subsingleton, iff_not_comm,
    ← Module.rank_pos_iff_of_free (R := R), pos_iff_ne_zero]

Premises used: iff_not_comm, Module.rank_pos_iff_of_free, not_nontrivial_iff_subsingleton, pos_iff_ne_zero
-- 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 : StrongRankCondition R
h : Basis ι R M
rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
rw₁ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{v, w} #ι)
rw₂ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{w, v} (Module.rank R M))
rw₃ : finrank R M = (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M)
rw₄ rw₅ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank R M = Nat.card ι

Tactic:
rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]

Premises used: Module.Basis.mk_eq_rank, Nat.card, Cardinal.toNat_lift, Module.finrank
-- 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 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
⊢ finrank R M = Fintype.card ι

Tactic:
finrank_eq_of_rank_eq (rank_eq_card_basis h)

Premises used: rank_eq_card_basis, Module.finrank_eq_of_rank_eq
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
ι : Type w
h : Basis ι R M
intro : ∀ (val : Fintype ι), (↑(finrank R M) : Cardinal.{w}) = #ι
⊢ (↑(finrank R M) : Cardinal.{w}) = #ι

Tactic:
cases @nonempty_fintype _ (Module.Finite.finite_basis h)

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 : StrongRankCondition R
inst_4 : Module.Finite R M
ι : Type w
h : Basis ι R M
val : Fintype ι
intro : Eq.{w + 2} (α := Cardinal.{w}) (↑(finrank R M) : Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w})
intro₁ intro₂ : Eq.{w + 2} (α := Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w})
⊢ (↑(finrank R M) : Cardinal.{w}) = #ι

Tactic:
rw [Cardinal.mk_fintype, finrank_eq_card_basis h]

Premises used: Module.finrank_eq_card_basis, 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 : StrongRankCondition R
ι : Type w
b : Finset ι
h : Basis.{w, u, v} (↥b) R M
rw : Fintype.card.{w} ↥b = b.card
rw₁ rw₂ : b.card = b.card
⊢ finrank R M = b.card

Tactic:
rw [finrank_eq_card_basis h, Fintype.card_coe]

Premises used: Module.finrank_eq_card_basis, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
rw : Cardinal.lift.{u, u} (Module.rank R R) = Cardinal.lift.{u, u} 1
rw₁ : Cardinal.lift.{u, u} #PUnit.{u + 1} = Cardinal.lift.{u, u} 1
rw₂ rw₃ : Cardinal.lift.{u, u} 1 = Cardinal.lift.{u, u} 1
⊢ Module.rank R R = 1

Tactic:
rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]

Premises used: Module.Basis.mk_eq_rank, Cardinal.lift_inj, PUnit, Module.Basis.singleton, Cardinal.mk_punit
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
⊢ Module.rank R R = (↑1 : Cardinal.{u})

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
inst_3 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
rw : finrank R R = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ finrank R M = 1

Tactic:
rw [← (LinearEquiv.ofBijective _ h).finrank_eq, finrank_self]

Premises used: LinearEquiv.finrank_eq, Module.finrank_self, LinearEquiv.ofBijective
-- 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 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
rw : finrank R M = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Module.rank R M = 1

Tactic:
rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_toSpanSingleton h]

Premises used: Module.finrank_of_bijective_toSpanSingleton, Module.rank_eq_one_iff_finrank_eq_one
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
h : Bijective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : finrank R R = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ finrank R S = 1

Tactic:
rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) h).toLinearEquiv.finrank_eq, finrank_self]

Premises used: AlgEquiv.ofBijective, LinearEquiv.finrank_eq, Algebra.ofId, AlgEquiv.toLinearEquiv, Module.finrank_self