awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Finite.{v + 1} (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this : Fintype (↑w : Type v) := Fintype.ofFinite (↑w : Type v)
t : Finset ι
v' : (x : (↑(↑t : Set ι) : Type u_2)) → M := fun (x : (↑(↑t : Set ι) : Type u_2)) ↦ v (↑x : ι)
⊢ t.card ≤ Fintype.card.{v} (↑w : Type v)
have i' : LinearIndependent R v'
Tactic: have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Finite.{v + 1} (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this : Fintype (↑w : Type v) := Fintype.ofFinite (↑w : Type v)
t : Finset ι
v' : (x : (↑(↑t : Set ι) : Type u_2)) → M := fun (x : (↑(↑t : Set ι) : Type u_2)) ↦ v (↑x : ι)
i' : LinearIndependent R v'
⊢ t.card ≤ Fintype.card.{v} (↑w : Type v)
have s' : range v' ≤ (↑(span R w) : Set M)
Tactic: have s' : range v' ≤ span R w := (range_comp_subset_range _ _).trans s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have this : Finite ι
Tactic: haveI : Finite ι := i.finite_of_le_span_finite v w s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have rw : LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
  (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
Tactic: rw [Cardinal.mk_fintype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : range v ≤ (↑(span R w) : Set M)
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(Fintype.card ι) : Cardinal.{u_2})
    (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have simp : Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
Tactic: simp only [Nat.cast_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ #ι ≤ (↑(Fintype.card.{v} (↑w : Type v)) : Cardinal.{u_2})
have apply : range v ≤ (↑(span R w) : Set M)
Tactic: apply linearIndependent_le_span' v i w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
v : ι → M
i : LinearIndependent R v
w : Set M
inst_4 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ range v ≤ (↑(span R w) : Set M)
have rw : range v ≤ (↑⊤ : Set M)
Tactic: rw [s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have by_contra : ∀ (h : ¬#κ ≤ #ι), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 : ¬#κ ≤ #ι
⊢ False
have h₁ : #(Finset ι) < #κ
Tactic: rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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))
⊢ False
have obtain : ∀ (s : Finset ι) (w : Infinite.{w + 1} (↑(Φ ⁻¹' {s}) : Type w)), False
Tactic: obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber' Φ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 : κ)
⊢ False
have i' : LinearIndependent R v'
Tactic: have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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)
have apply : range v' ≤ (↑(span R (↑(Finset.image (⇑b : (a : ι) → M) s) : Set M)) : Set M)
Tactic: apply i'.finite_of_le_span_finite v' (s.image b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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))
p : κ
w : Infinite.{w + 1} (↑(Φ ⁻¹' {Φ p}) : Type w)
v' : (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) → M := fun (k : (↑(Φ ⁻¹' {Φ p}) : Type w)) ↦ v (↑k : κ)
i' : LinearIndependent R v'
⊢ v' (Subtype.mk (p := fun (x : κ) ↦ x ∈ Φ ⁻¹' {Φ p}) p ⋯) ∈
    (↑(span R (↑(Finset.image (⇑b : (a : ι) → M) (Φ p)) : Set M)) : Set M)
have simp : Membership.mem (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' (↑(Φ p) : Set ι)))
  (v' (Subtype.mk (p := fun (x : κ) ↦ x ∈ Φ ⁻¹' {Φ p}) p sorry))
Tactic: simp only [SetLike.mem_coe, Finset.coe_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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'
⊢ False
have w' : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have by_contra : ¬#κ ≤ #ι → 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have by_contra₃ : ∀ (h : #(Finset ι) < #κ), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ ≤ #ι
have 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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 }
⊢ #α ≤ #β
have 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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
have 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)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 }
⊢ Injective (α := α →₀ R) (β := β →₀ R)
    (⇑(linearCombination R fun (i : α) ↦ (f : (a : α →₀ R) → β →₀ R) (single i 1)) : (a : α →₀ R) → β →₀ R)
have this : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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) ⊤
⊢ #ι ≤ #(↑w : Type v)
have f : (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
Tactic: fapply card_le_of_injective'' (R := R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #ι ≤ #(↑w : Type v)
have 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) sorry)) :
    (a : ι →₀ R) → (↑w : Type v) →₀ R)
Tactic: fapply card_le_of_injective'' (R := R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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) ⊤
⊢ (ι →₀ R) →ₗ[R] Finsupp.{v, u} (↑w : Type v) R
have f : ι → Finsupp.{v, u} (↑w : Type v) R
Tactic: apply Finsupp.linearCombination
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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)
⊢ f = g
have 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) sorry) :
            (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) sorry) :
            (a : ι →₀ R) → (↑w : Type v) →₀ R)
          g :
        Finsupp.{v, u} (↑w : Type v) R) :
    M)
Tactic: apply_fun linearCombination R ((↑) : w → M) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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)
⊢ f = g
have 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)
Tactic: simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #κ = #ι
have a : #κ ≤ #ι
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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 : #κ ≤ #ι
⊢ #κ = #ι
have a₁ : #ι ≤ #κ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
⊢ #ι ≤ #κ
have this : Nontrivial R
Tactic: haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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
⊢ #ι = Module.rank R M
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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
⊢ #ι = Module.rank R M
have rw : #ι = ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
Tactic: rw [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
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 }), #(↑(↑ι : Set M) : Type v)
have a : #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
Tactic: apply le_antisymm