awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (hypothesis)
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
⊢ LinearIndependent R b
have this : Module.Finite R M
Tactic: have := Module.Finite.of_surjective _ spans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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
⊢ LinearIndependent R b
have have : ∀ (f : Fin (Fintype.card ι) → M) (hf : LinearIndependent R f), LinearIndependent R b
Tactic: have ⟨f, hf⟩ := exists_linearIndependent_of_le_finrank card_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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
have 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) sorry)) :
          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: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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)
⊢ 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)
have 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) sorry))) :
    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)
Tactic: rwa [← map_coe, ← span_image, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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)
⊢ 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)
have 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) sorry))) :
    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)
Tactic: rwa [← map_coe, ← span_image, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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)
⊢ 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)
have 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) sorry))) :
    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)
Tactic: rwa [← map_coe, ← span_image, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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
⊢ LinearIndependent R b ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)
have rw : Fintype.card ι = Set.finrank R (Set.range b) ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (goal)
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)
⊢ LinearIndependent R b ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)
have rw₁ : Fintype.card ι = Set.finrank R (Set.range b) ↔ Fintype.card ι = Set.finrank R (Set.range b)
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).ge_iff_eq']
-- 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
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
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
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inl : ∀ (val : Fintype ι), lift.{w', w} #ι = lift.{w, w'} #ι'
Tactic: cases fintypeOrInfinite ι
-- 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
ι : 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'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inr : Infinite ι → lift.{w', w} #ι = lift.{w, w'} #ι'
Tactic: cases fintypeOrInfinite ι
-- 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
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val : Fintype ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have this₁ : Finite ι'
Tactic: haveI := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
-- 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
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this_1 : Nontrivial R
val : Fintype ι
this : Finite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inl : ∀ (val : Fintype ι'), lift.{w', w} #ι = lift.{w, w'} #ι'
Tactic: cases nonempty_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
ι : 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 ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inl : lift.{w', w} (↑(Fintype.card ι) : Cardinal.{w}) = lift.{w, w'} (↑(Fintype.card ι') : Cardinal.{w'})
Tactic: rw [Cardinal.mk_fintype, 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
ι : 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 ι'
⊢ lift.{w', w} (↑(Fintype.card ι) : Cardinal.{w}) = lift.{w, w'} (↑(Fintype.card ι') : Cardinal.{w'})
have inl : Fintype.card ι = Fintype.card ι'
Tactic: simp only [Cardinal.lift_natCast, Nat.cast_inj]
-- 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
ι : 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 ι'
⊢ Fintype.card ι = Fintype.card ι'
have inl : (ι → R) ≃ₗ[R] ι' → R
Tactic: apply card_eq_of_linearEquiv 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
ι : 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'} #ι'
have w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
Tactic: have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
-- 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
ι : 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'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inr : ∀ (f : ι ↪ ι'), lift.{w', w} #ι = lift.{w, w'} #ι'
Tactic: rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
-- 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
ι : 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 : ι ↪ ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have this₁ : Infinite ι'
Tactic: haveI : Infinite ι' := Infinite.of_injective f f.2
-- 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
ι : 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'} #ι'
have w₂ : lift.{w, w'} #ι' ≤ lift.{w', w} #ι
Tactic: have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
-- 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
ι : Type w
ι' : Type w'
inst_3 : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have haveI : ∀ (this : Nontrivial R), 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₂
-- 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
ι : 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'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inl : ∀ (this : Nontrivial R) (val : Fintype ι), 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₂
-- 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
ι : 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'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
have inr : ∀ (this : Nontrivial R), Infinite ι → 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₂
-- 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 : RankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
w : Set M
inst_5 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
have f : Finsupp.{v, u} (↑w : Type v) R →ₗ[R] ι →₀ R
Tactic: fapply card_le_of_surjective' 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 : RankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
w : Set M
inst_5 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
f : Finsupp.{v, u} (↑w : Type v) R →ₗ[R] ι →₀ R
⊢ Fintype.card ι ≤ Fintype.card.{v} (↑w : Type v)
have i : Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := ι →₀ R)
  (⇑((↑b.repr : M →ₗ[R] ι →₀ R) ∘ₗ Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) :
    (a : (↑w : Type v) →₀ R) → ι →₀ R)
Tactic: fapply card_le_of_surjective' 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 : RankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
w : Set M
inst_5 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
⊢ Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := ι →₀ R)
    (⇑((↑b.repr : M →ₗ[R] ι →₀ R) ∘ₗ Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) :
      (a : (↑w : Type v) →₀ R) → ι →₀ R)
have i : Surjective (α := M) (β := ι →₀ R) (⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R)
Tactic: apply Surjective.comp (g := b.repr.toLinearMap)
-- 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 : RankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : Basis ι R M
w : Set M
inst_5 : Fintype (↑w : Type v)
s : Eq (α := Submodule R M) (span R w) ⊤
i : Surjective (α := M) (β := ι →₀ R) (⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R)
⊢ Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := ι →₀ R)
    (⇑((↑b.repr : M →ₗ[R] ι →₀ R) ∘ₗ Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) :
      (a : (↑w : Type v) →₀ R) → ι →₀ R)
have i₁ : Surjective (α := Finsupp.{v, u} (↑w : Type v) R) (β := M)
  (⇑(Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w))) : (a : (↑w : Type v) →₀ R) → M)
Tactic: apply Surjective.comp (g := b.repr.toLinearMap)