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
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
s : Finset ι
w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
⊢ Finite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)

Tactic:
have w' : Finite (Φ ⁻¹' {s}) := by
    apply i'.finite_of_le_span_finite v' (s.image b)
    rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
    simp only [SetLike.mem_coe, Finset.coe_image]
    apply Basis.mem_span_repr_support
-- 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 : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
s : Finset ι
w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
w' : Finite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
⊢ False

Tactic:
w.false

Premises used: Infinite.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
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
s : Finset ι
w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
w' : Finite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)
⊢ False

Tactic:
exact w.false

Premises used: Infinite.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
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
by_contra by_contra₁ by_contra₂ : ∀ (h : ¬#κ ≤ #ι), False
by_contra₃ : ∀ (h : #(Finset ι) < #κ), False
by_contra₄ : ∀ (h : #(Finset ι) < #κ), False
by_contra₅ by_contra₆ :
  ∀ (h : #(Finset ι) < #κ),
    let Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k));
    ∀ (s : Finset ι) (w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)), False
by_contra₇ :
  ∀ (h : #(Finset ι) < #κ),
    let Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k));
    ∀ (s : Finset ι) (w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)),
      let v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ);
      ∀ (i' : LinearIndependent R v'), False
by_contra₈ :
  ∀ (h : #(Finset ι) < #κ),
    let Φ : (k : κ) → Finset ι := fun (k : κ) ↦ Finsupp.support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k));
    ∀ (s : Finset ι) (w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)),
      let v' : (k : (↑(Φ ⁻¹' {s}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {s}) : Type w)) ↦ v (↑k : κ);
      ∀ (i' : LinearIndependent R v') (w' : Finite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)), False
⊢ #κ ≤ #ι

Tactic:
classical
  by_contra h
  rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
  let Φ := fun k : κ => (b.repr (v k)).support
  obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber' Φ h
  let v' := fun k : Φ ⁻¹' {s} => v k
  have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
  have w' : Finite (Φ ⁻¹' {s}) := by
    apply i'.finite_of_le_span_finite v' (s.image b)
    rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
    simp only [SetLike.mem_coe, Finset.coe_image]
    apply Basis.mem_span_repr_support
  exact w.false

Premises used: not_le, Cardinal.mk_finset_of_infinite
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b : Basis β R (β →₀ R) := { repr := 1 }
apply : LinearIndependent R (M := β →₀ R) fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)
⊢ #α ≤ #β

Tactic:
apply linearIndependent_le_basis b (fun (i : α) ↦ f (Finsupp.single i 1))

Premises used: linearIndependent_le_basis, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b : Basis β R (β →₀ R) := { repr := 1 }
h :
  ∀ (a : α) (b : β),
    Eq.{u + 1} (α := R)
      ((((linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) ∘ₗ lsingle a : (a : R) → β →₀ R)
              1 :
            (a : β) → R)
          b :
        R)
      (((f ∘ₗ lsingle a : (a : R) → β →₀ R) 1 : (a : β) → R) b : R)
⊢ (linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) = f

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b_1 : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ Eq.{u + 1} (α := R)
    ((((linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) ∘ₗ lsingle a : (a : R) → β →₀ R) 1 :
          (a : β) → R)
        b :
      R)
    (((f ∘ₗ lsingle a : (a : R) → β →₀ R) 1 : (a : β) → R) b : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ (linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) = f

Tactic:
have : (linearCombination R fun i ↦ f (Finsupp.single i 1)) = f := by ext a b; simp
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b : Basis β R (β →₀ R) := { repr := 1 }
this : (linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) = f
⊢ Injective (α := α →₀ R) (β := β →₀ R)
    (⇑(linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) : (a : α →₀ R) → β →₀ R)

Tactic:
this.symm ▸ i

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
b : Basis β R (β →₀ R) := { repr := 1 }
this : (linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) = f
⊢ Injective (α := α →₀ R) (β := β →₀ R)
    (⇑(linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) : (a : α →₀ R) → β →₀ R)

Tactic:
exact this.symm ▸ i
-- 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 v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f : (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
i₁ :
  Injective (α := ι →₀ R) (β := Finsupp.{v, u} (↑w : Type v) R)
    (⇑(linearCombination R fun (i : ι) ↦
          Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯)) :
      (a : ι →₀ R) → (↑w : Type v) →₀ R)
⊢ #ι ≤ #(↑w : Type v)

Tactic:
fapply card_le_of_injective'' (R := R)

Premises used: card_le_of_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
inst_3 : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f : ι → Finsupp.{v, u} (↑w : Type v) R
⊢ (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R

Tactic:
apply Finsupp.linearCombination

Premises used: Finsupp.linearCombination
-- 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 v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ ι → Finsupp.{v, u} (↑w : Type v) R

Tactic:
exact fun i ↦ Span.repr R w ⟨v i, s ▸ trivial⟩

Premises used: Span.repr, Subtype.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
inst_3 : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f g : ι →₀ R
h :
  Eq (α := Finsupp.{v, u} (↑w : Type v) R)
    ((linearCombination R fun (i : ι) ↦
            Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
          (a : ι →₀ R) → (↑w : Type v) →₀ R)
        f :
      Finsupp.{v, u} (↑w : Type v) R)
    ((linearCombination R fun (i : ι) ↦
            Span.repr R w (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
          (a : ι →₀ R) → (↑w : Type v) →₀ R)
        g :
      Finsupp.{v, u} (↑w : Type v) R)
⊢ Eq.{v + 1} (α := M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            f :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            g :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)

Tactic:
apply_fun linearCombination R ((↑) : w → M) at h

Premises used: Finsupp.linearCombination, Subtype.val
-- 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 v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            f :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
    ((linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
        ((linearCombination R fun (i : ι) ↦
                Span.repr R w
                  (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R w) x) (v i) ⋯) :
              (a : ι →₀ R) → (↑w : Type v) →₀ R)
            g :
          Finsupp.{v, u} (↑w : Type v) R) :
      M)
⊢ Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)

Tactic:
simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h

Premises used: Span.finsupp_linearCombination_repr, Finsupp.linearCombination_linearCombination
-- 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 v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)
⊢ f = g

Tactic:
i h
-- 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 v
v : ι → M
i : LinearIndependent R v
w : Set M
s : Eq (α := Submodule R M) (span R w) ⊤
f g : ι →₀ R
h :
  Eq.{v + 1} (α := M) ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) f : M)
    ((linearCombination R fun (b : ι) ↦ v b : (a : ι →₀ R) → M) g : M)
⊢ f = g

Tactic:
exact i h
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StrongRankCondition R
n m : ℕ
v : Fin m → Fin n → R
h : LinearIndependent R v
⊢ m ≤ n

Tactic:
simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h

Premises used: linearIndependent_le_basis, Pi.basisFun, Fin
-- 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 : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
a : #κ ≤ #ι
a₁ : #ι ≤ #κ
⊢ #κ = #ι

Tactic:
apply le_antisymm

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
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ ≤ #ι

Tactic:
linearIndependent_le_basis b v i

Premises used: linearIndependent_le_basis
-- 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 : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ ≤ #ι

Tactic:
exact linearIndependent_le_basis b v i

Premises used: linearIndependent_le_basis
-- 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 : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := 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
inst_3 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
this : Nontrivial R
⊢ #ι ≤ #κ

Tactic:
infinite_basis_le_maximal_linearIndependent b v i m

Premises used: infinite_basis_le_maximal_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 : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
this : Nontrivial R
⊢ #ι ≤ #κ

Tactic:
exact infinite_basis_le_maximal_linearIndependent b v i m

Premises used: infinite_basis_le_maximal_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 : StrongRankCondition R
ι : Type v
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
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
rw : #ι = ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
⊢ #ι = Module.rank R M

Tactic:
rw [Module.rank_def]

Premises used: Module.rank_def
-- 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 v
v : Basis ι R M
this : Nontrivial R
a : #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
a₁ : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) ≤ #ι
⊢ #ι = ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)

Tactic:
apply le_antisymm

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
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
trans :
  #ι ≤
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v)
trans₁ :
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
trans₂ : Cardinal.{v}
⊢ #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)

Tactic:
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
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
apply : { s : Set M // LinearIndepOn R id s }
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)

Tactic:
apply le_ciSup Cardinal.bddAbove_of_small

Premises used: le_ciSup, Cardinal.bddAbove_of_small
-- 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 v
v : Basis ι R M
this : Nontrivial R
⊢ LinearIndependent.{v, u, v} (ι := (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)) R (M := M)
    (⇑v.reindexRange : (a : (↑(range (⇑v : (a : ι) → M)) : Type v)) → M)

Tactic:
v.reindexRange.linearIndependent

Premises used: Module.Basis.reindexRange, 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 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
h :
  ∀ (x : (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)),
    id (↑x : M) = (v.reindexRange : (a : (↑(range (⇑v : (a : ι) → M)) : Type v)) → M) x
⊢ LinearIndependent R (M := M) fun (x : (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)) ↦ id (↑x : M)

Tactic:
convert! v.reindexRange.linearIndependent

Premises used: Module.Basis.reindexRange, 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 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
x : (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ id (↑x : M) = (v.reindexRange : (a : (↑(range (⇑v : (a : ι) → M)) : Type v)) → M) x

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
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ { s : Set M // LinearIndepOn R id s }

Tactic:
exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert! v.reindexRange.linearIndependent
          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
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v)

Tactic:
(Cardinal.mk_range_eq v v.injective).ge

Premises used: Eq.ge, setOf, Module.Basis.injective, Set.range, DFunLike.coe, Cardinal.mk_range_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
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v)

Tactic:
exact (Cardinal.mk_range_eq v v.injective).ge

Premises used: Eq.ge, Module.Basis.injective, DFunLike.coe, Cardinal.mk_range_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
ι : Type v
v : Basis ι R M
this : Nontrivial R
a : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ #ι
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) ≤ #ι

Tactic:
apply ciSup_le'

Premises used: ciSup_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
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
s : Set M
li : LinearIndepOn R id s
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s li) : Set M) : Type v) ≤ #ι

Tactic:
apply linearIndependent_le_basis v _ li

Premises used: linearIndependent_le_basis
-- 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
⊢ #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v) = Module.rank R M

Tactic:
v.reindexRange.mk_eq_rank''

Premises used: Module.Basis.reindexRange, Module.Basis.mk_eq_rank''
-- 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
⊢ 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
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
this : Nontrivial R
rw : #(↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v) = (↑(Fintype.card ι) : Cardinal.{v})
rw₁ :
  Eq.{v + 2} (α := Cardinal.{v})
    (↑(Fintype.card.{v} (↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v)) : Cardinal.{v})
    (↑(Fintype.card ι) : Cardinal.{v})
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) (↑(Fintype.card ι) : Cardinal.{v}) (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})

Tactic:
rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

Premises used: Module.Basis.mk_range_eq_rank, Module.Basis.injective, Set.card_range_of_injective, Cardinal.mk_fintype