awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
x : K₃
mpr :
  Eq.{u_11 + 1} (α := C₂) ((G ∘ₗ π₁ : (a : N₁) → C₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₂)
    (0 : C₂)
mpr₁ :
  Eq.{u_11 + 1} (α := C₂) ((π₂ ∘ₗ g₁ : (a : N₁) → C₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₂)
    (0 : C₂)
mpr₂ :
  Eq.{u_11 + 1} (α := C₂)
    ((π₂ : (a : N₂) → C₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂) : C₂)
    (0 : C₂)
mpr₃ :
  Eq.{u_11 + 1} (α := C₂) ((π₂ : (a : N₂) → C₂) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂) : C₂) (0 : C₂)
⊢ Eq.{u_11 + 1} (α := C₂)
    ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁) : C₂)
    (0 : C₂)
have mpr₄ : Eq.{u_11 + 1} (α := C₂) 0 0
Tactic: rw [← G.comp_apply, hF, π₂.comp_apply, H₂, hπ₂.apply_apply_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
have a : LE.le (α := ℕ∞)
  ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
  (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
a :
  LE.le (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
⊢ Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
have a₁ : LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
  ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ LE.le (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
have a : ∀ (s : Set M) (hs : span R s = p),
  (toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) ≤ s.encard
Tactic: refine le_iInf₂ (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
have this : Eq (α := ℕ∞) (id (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
  (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
Tactic: have := congrFun toENat_comp_ofENat.{u}.symm (⨅ (s : Set M) (_ : span R s = p), s.encard)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
this :
  Eq (α := ℕ∞) (id (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
    (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
⊢ LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
have this₁ : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
  (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
Tactic: rw [id_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
this :
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
⊢ LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
have a : LE.le (α := ℕ∞) (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : ℕ∞)
  ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
this :
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
⊢ LE.le (α := ℕ∞) (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
have a : ∀ (s : { s : Set M // span R s = p }),
  (↑(⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)
Tactic: refine toENat.monotone' (le_ciInf fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
this :
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
s : { s : Set M // span R s = p }
⊢ (↑(⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)
have this₁ : (↑(⨅ (s' : Set M), ⨅ (_ : span R s' = p), s'.encard) : Cardinal.{u}) ≤ (↑(↑s : Set M).encard : Cardinal.{u})
Tactic: have : ofENat.{u} (⨅ (s' : Set M), ⨅ (_ : span R s' = p), s'.encard) ≤ ofENat s.1.encard :=
      ofENatHom.monotone' (le_trans (ciInf_le' _ s.1) (ciInf_le' _ s.2))
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
this_1 :
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (((⇑toENat : (a : Cardinal.{u}) → ℕ∞) ∘ ofENat) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard))
s : { s : Set M // span R s = p }
this : (↑(⨅ (s' : Set M), ⨅ (_ : span R s' = p), s'.encard) : Cardinal.{u}) ≤ (↑(↑s : Set M).encard : Cardinal.{u})
⊢ (↑(⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)
have a : (↑(↑s : Set M).encard : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)
Tactic: apply le_trans this
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) p.spanRank : ℕ∞)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞) : ℕ∞)
have rw : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
  (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
Tactic: rw [spanRank_toENat_eq_iInf_encard]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
have inl : ∀ (h1 : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤),
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
Tactic: rcases eq_or_ne (⨅ (s : Set M) (_ : span R s = p), s.encard) ⊤ with (h1 | h2)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
inl :
  ∀ (h1 : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤),
    Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
      (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
have inr : ∀ (h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤),
  Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
Tactic: rcases eq_or_ne (⨅ (s : Set M) (_ : span R s = p), s.encard) ⊤ with (h1 | h2)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h1 : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
have inl : Eq (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞)) ⊤
Tactic: rw [h1, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h1 : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
⊢ Eq (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞)) ⊤
have inl : ∀ (h1 : ∀ (i : Set M) (i_1 : span R i = p), i.encard = ⊤) (i : { s : Finset M // span R (↑s : Set M) = p }),
  Eq (α := ℕ∞) (↑(↑i : Finset M).card : ℕ∞) ⊤
Tactic: simp_rw [iInf_eq_top] at h1 ⊢
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞))
have inr : Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
  (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
Tactic: simp_rw [← Set.encard_coe_eq_coe_finsetCard]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
have inr : LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
  (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
inr :
  LE.le (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
⊢ Eq (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
have inr₁ : LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
  (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
⊢ LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard)
    (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard)
have inr : ∀ (s : Set M) (h : span R s = p),
  ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
Tactic: refine le_iInf fun s ↦ le_iInf fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
s : Set M
h : span R s = p
⊢ ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
have pos : ∀ (hs : s.Finite), ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
s : Set M
h : span R s = p
pos :
  ∀ (hs : s.Finite), ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
⊢ ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
have neg : ∀ (hs : ¬s.Finite), ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h2 : Ne (α := ℕ∞) (⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard
have neg : LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard) ⊤
Tactic: rw [Set.Infinite.encard_eq hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ p.spanRank < ℵ₀ ↔ p.FG
have rw : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ ↔ ∃ (S : Set M), S.Finite ∧ span R S = p
Tactic: rw [spanRank, Submodule.fg_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ ↔ ∃ (S : Set M), S.Finite ∧ span R S = p
have mp : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ → ∃ (S : Set M), S.Finite ∧ span R S = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
mp : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ → ∃ (S : Set M), S.Finite ∧ span R S = p
⊢ ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ ↔ ∃ (S : Set M), S.Finite ∧ span R S = p
have mpr : (∃ (S : Set M), S.Finite ∧ span R S = p) → ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
⊢ ∃ (S : Set M), S.Finite ∧ span R S = p
have mp : ∀ (s : { s : Set M // span R s = p })
  (hs :
    Eq.{u + 2} (α := Cardinal.{u})
      ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
      (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))),
  ∃ (S : Set M), S.Finite ∧ span R S = p
Tactic: obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
⊢ ∃ (S : Set M), S.Finite ∧ span R S = p
have mp : (↑s : Set M).Finite
Tactic: refine ⟨s.1, ?_, s.2⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ p.spanFinrank = 0
have refine : p.spanRank = 0 ∨ ℵ₀ ≤ p.spanRank
Tactic: refine toNat_eq_zero.2 ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ p.spanRank = 0 ∨ ℵ₀ ≤ p.spanRank
have h : ℵ₀ ≤ p.spanRank
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ ℵ₀ ≤ p.spanRank
have h : ∀ (h : p.spanRank < ℵ₀), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ p.spanRank = (↑p.spanFinrank : Cardinal.{u}) ↔ p.FG
have rw : (↑((toNat : (a : Cardinal.{u}) → ℕ) p.spanRank) : Cardinal.{u}) = p.spanRank ↔ p.spanRank < ℵ₀
Tactic: rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
⊢ spanRank (span R (Set.range v)) = #ι
have refine : ∀ (x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }), #ι ≤ #(↑(↑x : Set M) : Type u)
Tactic: refine le_antisymm (le_trans (spanRank_span_le_card _) mk_range_le) (le_ciInf fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
⊢ #ι ≤ #(↑(↑x : Set M) : Type u)
have this : #(↑(↑x : Set M) : Type u) =
  #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹' (↑x : Set M)) :
      Type u)
Tactic: have : #x.1 = #((Subtype.val : span R (.range v) → _) ⁻¹' x.1) :=
    (mk_preimage_of_injective_of_subset_range _ _ Subtype.val_injective (by simp [← x.2])).symm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ #ι ≤ #(↑(↑x : Set M) : Type u)
have rw : #ι ≤
  #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹' (↑x : Set M)) :
      Type u)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ #ι ≤
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
have refine_1 : #ι ≤ #(↑(Set.range (ι := ι) (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))) : Type u)
Tactic: refine le_trans ?_ ((Module.Basis.span hs).le_span (R := R) (J := Subtype.val ⁻¹' x.1) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
refine_1 : #ι ≤ #(↑(Set.range (ι := ι) (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))) : Type u)
⊢ #ι ≤
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
have refine_2 : Eq (α := Submodule R ↥(span R (Set.range v)))
  (span R
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹' (↑x : Set M)))
  ⊤
Tactic: refine le_trans ?_ ((Module.Basis.span hs).le_span (R := R) (J := Subtype.val ⁻¹' x.1) ?_)