awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₄ :
  ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₅ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₆ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R))
    (n : ℕ), (↑n : Cardinal.{u_1}) ≤ Module.rank R R
rw₇ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R))
    (n : ℕ), LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
rw₈ rw₉ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)) (n : ℕ)
    (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    simpa only [dif_pos i.prop] using this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0
      (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim

Premises used: Iff.mpr, neg_eq_iff_add_eq_zero, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors, pow_succ, add_assoc, mul_assoc, Cardinal.aleph0_le, zero_add, not_nonempty_iff, zero_smul, neg_mul, smul_eq_mul, add_zero, Finset.sum_range_succ', Not, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
by_contra! : ∀ (h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), False
⊢ Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))

Tactic:
by_contra! h
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
have := aleph0_le_rank_of_isEmpty_oreSet h
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
this : ℵ₀ ≤ Module.rank R R
⊢ ℵ₀ ≤ 1

Tactic:
rw [rank_self] at this

Premises used: Module.rank_self
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
this : ℵ₀ ≤ 1
⊢ False

Tactic:
this.not_gt one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, LE.le.not_gt
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
this : ℵ₀ ≤ 1
⊢ False

Tactic:
exact this.not_gt one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, LE.le.not_gt
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : LE.le (α := Submodule R M) ⊤ (span R (Set.range b))
card_le : Fintype.card ι ≤ finrank R M
⊢ Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)

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

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination, top_le_iff
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : LE.le (α := Submodule R M) ⊤ (span R (Set.range b))
card_le : Fintype.card ι ≤ finrank R M
spans₁ : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
⊢ Fintype.card ι ≤ finrank R M

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

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination, top_le_iff
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
card_le : Fintype.card ι ≤ finrank R M
⊢ Module.Finite R M

Tactic:
have := Module.Finite.of_surjective _ spans
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
card_le : Fintype.card ι ≤ finrank R M
this : Module.Finite R M
have : ∀ (f : Fin (Fintype.card ι) → M) (hf : LinearIndependent R f), LinearIndependent R b
⊢ LinearIndependent R b

Tactic:
have ⟨f, hf⟩ := exists_linearIndependent_of_le_finrank card_le
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
card_le : Fintype.card ι ≤ finrank R M
this : Module.Finite R M
f : Fin (Fintype.card ι) → M
hf : LinearIndependent R f
⊢ LinearIndependent R b

Tactic:
OrzechProperty.injective_of_surjective_of_injective
    _ _ (hf.comp _ (Fintype.equivFin _).injective) spans

Premises used: OrzechProperty.injective_of_surjective_of_injective, Fintype.equivFin, LinearIndependent, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
card_le : Fintype.card ι ≤ finrank R M
this : Module.Finite R M
f : Fin (Fintype.card ι) → M
hf : LinearIndependent R f
⊢ LinearIndependent R b

Tactic:
exact OrzechProperty.injective_of_surjective_of_injective
    _ _ (hf.comp _ (Fintype.equivFin _).injective) spans

Premises used: OrzechProperty.injective_of_surjective_of_injective, Fintype.equivFin, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : LE.le (α := Submodule R M) ⊤ (span R (Set.range b))
card_eq : Fintype.card ι = finrank R M
⊢ LinearIndependent R b

Tactic:
linearIndependent_of_top_le_span_of_card_le_finrank spans card_eq.le

Premises used: linearIndependent_of_top_le_span_of_card_le_finrank, Eq.le
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Nontrivial R
ι : Type u_3
inst_5 : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
⊢ LinearIndependent R b

Tactic:
(LinearMap.linearIndependent_iff_of_injOn _ (subtype_injective _).injOn).mpr <|
      linearIndependent_of_top_le_span_of_card_eq_finrank (b := fun i ↦ ⟨b i, subset_span ⟨i, rfl⟩⟩)
        (fun ⟨_, _⟩ _ ↦ (subtype_injective _).mem_set_image.mp ?_) hc

Premises used: Iff.mpr, linearIndependent_of_top_le_span_of_card_eq_finrank, Function.Injective.injOn, LinearMap.linearIndependent_iff_of_injOn, Submodule.subtype_injective
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Nontrivial R
ι : Type u_3
inst_5 : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
refine :
  ∀ (x : ↥(span R (Set.range b))) (val : M) (property : Membership.mem (γ := Submodule R M) (span R (Set.range b)) val),
    Membership.mem (γ := Submodule R ↥(span R (Set.range b))) ⊤
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property) →
      Membership.mem (α := M) (γ := Set M)
        ((⇑(Submodule.subtype (span R (Set.range b))) : (a : ↥(span R (Set.range b))) → M) ''
          (↑(span R
                (Set.range fun (i : ι) ↦
                  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) (b i)
                    ⋯)) :
            Set ↥(span R (Set.range b))))
        ((Submodule.subtype (span R (Set.range b)) : (a : ↥(span R (Set.range b))) → M)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val
              property) :
          M)
⊢ LinearIndependent R b

Tactic:
refine (LinearMap.linearIndependent_iff_of_injOn _ (subtype_injective _).injOn).mpr <|
      linearIndependent_of_top_le_span_of_card_eq_finrank (b := fun i ↦ ⟨b i, subset_span ⟨i, rfl⟩⟩)
        (fun ⟨_, _⟩ _ ↦ (subtype_injective _).mem_set_image.mp ?_) hc

Premises used: Iff.mpr, linearIndependent_of_top_le_span_of_card_eq_finrank, Function.Injective.injOn, LinearMap.linearIndependent_iff_of_injOn, Submodule.subtype_injective
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Nontrivial R
ι : Type u_3
inst_5 : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x : ↥(span R (Set.range b))
val : M
property : Membership.mem (γ := Submodule R M) (span R (Set.range b)) val
h :
  Membership.mem (γ := Submodule R ↥(span R (Set.range b))) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property)
rwa :
  Membership.mem (α := M)
    (↑(map (M := ↥(span R (Set.range b))) (Submodule.subtype (span R (Set.range b)))
          (span R
            (Set.range fun (i : ι) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) (b i) ⋯))) :
      Set M)
    ((Submodule.subtype (span R (Set.range b)) : (a : ↥(span R (Set.range b))) → M)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property) :
      M)
rwa₁ :
  Membership.mem (α := M)
    (↑(span R
          (Set.image (α := ↥(span R (Set.range b)))
            (⇑(Submodule.subtype (span R (Set.range b))) : (a : ↥(span R (Set.range b))) → M)
            (Set.range fun (i : ι) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) (b i) ⋯))) :
      Set M)
    ((Submodule.subtype (span R (Set.range b)) : (a : ↥(span R (Set.range b))) → M)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property) :
      M)
rwa₂ rwa₃ rwa₄ rwa₅ :
  Membership.mem (α := M)
    (↑(span R
          (Set.range.{u_2, u_3 + 1} (ι := ι)
            (Function.comp (β := ↥(span R (Set.range b)))
              (⇑(Submodule.subtype (span R (Set.range b))) : (a : ↥(span R (Set.range b))) → M) fun (i : ι) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) (b i) ⋯))) :
      Set M)
    ((Submodule.subtype (span R (Set.range b)) : (a : ↥(span R (Set.range b))) → M)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property) :
      M)
⊢ Membership.mem (α := M) (γ := Set M)
    ((⇑(Submodule.subtype (span R (Set.range b))) : (a : ↥(span R (Set.range b))) → M) ''
      (↑(span R
            (Set.range fun (i : ι) ↦
              Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) (b i) ⋯)) :
        Set ↥(span R (Set.range b))))
    ((Submodule.subtype (span R (Set.range b)) : (a : ↥(span R (Set.range b))) → M)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range b)) x) val property) :
      M)

Tactic:
rwa [← map_coe, ← span_image, ← Set.range_comp]

Premises used: Set.range_comp, Submodule.span_image, Submodule.map_coe
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Nontrivial R
ι : Type u_3
inst_5 : Fintype ι
b : ι → M
rw : Fintype.card ι = Set.finrank R (Set.range b) ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)
rw₁ rw₂ : Fintype.card ι = Set.finrank R (Set.range b) ↔ Fintype.card ι = Set.finrank R (Set.range b)
⊢ LinearIndependent R b ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)

Tactic:
rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).ge_iff_eq']

Premises used: finrank_range_le_card, LE.le.ge_iff_eq', linearIndependent_iff_card_eq_finrank_span
-- Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
le_span : LE.le (α := Submodule R M) ⊤ (span R (Set.range b))
card_eq : Fintype.card ι = finrank R M
⊢ (⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) : (a : ι) → M) = b

Tactic:
Basis.coe_mk _ _

Premises used: Module.Basis.coe_mk
-- 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 : InvariantBasisNumber R
v : Basis ι R M
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
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
inl : ∀ (val : Fintype ι), lift.{w', w} #ι = lift.{w, w'} #ι'
inr : Infinite ι → lift.{w', w} #ι = lift.{w, w'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
cases fintypeOrInfinite ι

Premises used: fintypeOrInfinite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val : Fintype ι
⊢ Finite ι'

Tactic:
haveI := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
inl : ∀ (val : Fintype ι'), lift.{w', w} #ι = lift.{w, w'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
cases nonempty_fintype ι'

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
val_1 : Fintype ι'
inl : lift.{w', w} (↑(Fintype.card ι) : Cardinal.{w}) = lift.{w, w'} (↑(Fintype.card ι') : Cardinal.{w'})
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
rw [Cardinal.mk_fintype, Cardinal.mk_fintype]

Premises used: Cardinal.mk_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
val_1 : Fintype ι'
inl : Fintype.card ι = Fintype.card ι'
⊢ lift.{w', w} (↑(Fintype.card ι) : Cardinal.{w}) = lift.{w, w'} (↑(Fintype.card ι') : Cardinal.{w'})

Tactic:
simp only [Cardinal.lift_natCast, Nat.cast_inj]

Premises used: Nat.cast_inj, Cardinal.lift_natCast
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
val_1 : Fintype ι'
inl : (ι → R) ≃ₗ[R] ι' → R
⊢ Fintype.card ι = Fintype.card ι'

Tactic:
apply card_eq_of_linearEquiv R

Premises used: card_eq_of_linearEquiv
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
val_1 : Fintype ι'
⊢ (ι → R) ≃ₗ[R] ι' → R

Tactic:
exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'

Premises used: LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Module.Basis.repr, LinearEquiv.trans
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val : Infinite ι
⊢ lift.{w', w} #ι ≤ lift.{w, w'} #ι'

Tactic:
have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
inr : ∀ (f : ι ↪ ι'), lift.{w', w} #ι = lift.{w, w'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩

Premises used: Iff.mp, Cardinal.lift_mk_le'
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
⊢ Infinite ι'

Tactic:
haveI : Infinite ι' := Infinite.of_injective f f.2
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
⊢ lift.{w, w'} #ι' ≤ lift.{w', w} #ι

Tactic:
have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift.{w, w'} #ι' ≤ lift.{w', w} #ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
le_antisymm w₁ w₂

Premises used: le_antisymm
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift.{w, w'} #ι' ≤ lift.{w', w} #ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
exact le_antisymm w₁ w₂

Premises used: le_antisymm
-- 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 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
haveI haveI₁ haveI₂ : ∀ (this : Nontrivial R), lift.{w', w} #ι = lift.{w, w'} #ι'
inl : ∀ (this : Nontrivial R) (val : Fintype ι), lift.{w', w} #ι = lift.{w, w'} #ι'
inr inr₁ : ∀ (this : Nontrivial R), Infinite ι → lift.{w', w} #ι = lift.{w, w'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
classical
  haveI := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite ι
  · -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
    -- haveI : Finite (range v) := Set.finite_range v
    haveI := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
    cases nonempty_fintype ι'
    -- We clean up a little:
    rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
    simp only [Cardinal.lift_natCast, Nat.cast_inj]
    -- Now we can use invariant basis number to show they have the same cardinality.
    apply card_eq_of_linearEquiv R
    exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'
  · -- `v` is an infinite basis,
    -- so by `infinite_basis_le_maximal_linearIndependent`, `v'` is at least as big,
    -- and then applying `infinite_basis_le_maximal_linearIndependent` again
    -- we see they have the same cardinality.
    have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
    rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
    haveI : Infinite ι' := Infinite.of_injective f f.2
    have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
    exact le_antisymm w₁ w₂

Premises used: card_eq_of_linearEquiv, Nat.cast_inj, Module.Basis.repr, Cardinal.mk_fintype, Cardinal.lift_natCast, fintypeOrInfinite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : InvariantBasisNumber R
ι' : Type w
v : Basis ι R M
v' : Basis ι' R M
⊢ #ι = #ι'

Tactic:
Cardinal.lift_inj.1 <| mk_eq_mk_of_basis v v'

Premises used: mk_eq_mk_of_basis, Cardinal.lift_inj, Iff.mp