awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.SnakeLemma
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₂
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : 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₁)
hf₂ : Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Injective.{u_5 + 1, u_6 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective.{u_9 + 1, u_4 + 1} (α := K₃) (β := M₃) (⇑ι₃ : (a : K₃) → M₃)
⊢ Exact.{u_8, u_9, u_10} (M := K₂) (N := K₃) (P := C₁) (⇑F : (a : K₂) → K₃)
    (⇑(δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁) : (a : K₃) → C₁)

Tactic:
SnakeLemma.exact_δ_right _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› _ _ _ _ _ ‹_› ‹_›

Premises used: SnakeLemma.exact_δ_right
-- Module: Mathlib.Algebra.Module.SnakeLemma
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₂
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₂)
hf₂ : Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Injective.{u_5 + 1, u_6 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
⊢ Exact.{u_9, u_10, u_11} (M := K₃) (N := C₁) (P := C₂)
    (⇑(δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁) : (a : K₃) → C₁) (⇑G : (a : C₁) → C₂)

Tactic:
SnakeLemma.exact_δ_left _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› _ ‹_› ‹_›

Premises used: SnakeLemma.exact_δ_left
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ span R (↑p : Set M) = p

Tactic:
simp
-- Module: Mathlib.Algebra.Module.SpanRank
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 : ℕ∞)
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)) : ℕ∞)
⊢ 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 : ℕ∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.SpanRank
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 : ℕ∞)

Tactic:
le_iInf₂ (fun s hs ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.Algebra.Module.SpanRank
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 :
  ∀ (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
⊢ 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:
refine le_iInf₂ (fun s hs ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.Algebra.Module.SpanRank
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 : Set M
hs : span R s = p
⊢ LE.le (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) #(↑s : Type u) : ℕ∞)

Tactic:
toENat.monotone' (ciInf_le' _ (⟨s, hs⟩ : {s : Set M // span R s = p}))

Premises used: ciInf_le', Subtype.mk, OrderRingHom.monotone', Cardinal.toENat
-- Module: Mathlib.Algebra.Module.SpanRank
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 : Set M
hs : span R s = p
⊢ LE.le (α := ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u)) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) #(↑s : Type u) : ℕ∞)

Tactic:
exact toENat.monotone' (ciInf_le' _ (⟨s, hs⟩ : {s : Set M // span R s = p}))

Premises used: ciInf_le', Subtype.mk, OrderRingHom.monotone', Cardinal.toENat
-- Module: Mathlib.Algebra.Module.SpanRank
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 (α := ℕ∞) (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)
-- Module: Mathlib.Algebra.Module.SpanRank
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))
⊢ 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

Premises used: id_eq
-- Module: Mathlib.Algebra.Module.SpanRank
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))
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)) : ℕ∞)
⊢ 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:
rw [this]
-- Module: Mathlib.Algebra.Module.SpanRank
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)) : ℕ∞)

Tactic:
toENat.monotone' (le_ciInf fun s ↦ ?_)

Premises used: le_ciInf, OrderRingHom.monotone', Cardinal.toENat
-- Module: Mathlib.Algebra.Module.SpanRank
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))
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)
⊢ 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:
refine toENat.monotone' (le_ciInf fun s ↦ ?_)

Premises used: le_ciInf, OrderRingHom.monotone', Cardinal.toENat
-- Module: Mathlib.Algebra.Module.SpanRank
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).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))
-- Module: Mathlib.Algebra.Module.SpanRank
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})
a : (↑(↑s : Set M).encard : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)
⊢ (↑(⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)

Tactic:
apply le_trans this

Premises used: le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
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})
⊢ (↑((toENat : (a : Cardinal.{u}) → ℕ∞) #(↑(↑s : Set M) : Type u)) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)

Tactic:
Cardinal.ofENat_toENat_le _

Premises used: Cardinal.ofENat_toENat_le
-- Module: Mathlib.Algebra.Module.SpanRank
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})
⊢ (↑((toENat : (a : Cardinal.{u}) → ℕ∞) #(↑(↑s : Set M) : Type u)) : Cardinal.{u}) ≤ #(↑(↑s : Set M) : Type u)

Tactic:
exact Cardinal.ofENat_toENat_le _

Premises used: Cardinal.ofENat_toENat_le
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
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 : ℕ∞))
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) p.spanRank : ℕ∞)
    (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞) : ℕ∞)

Tactic:
rw [spanRank_toENat_eq_iInf_encard]

Premises used: Submodule.spanRank_toENat_eq_iInf_encard
-- Module: Mathlib.Algebra.Module.SpanRank
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 : ℕ∞))
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 : ℕ∞))
⊢ 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)

Premises used: Set.encard, iInf, eq_or_ne, Top.top
-- Module: Mathlib.Algebra.Module.SpanRank
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) ⊤
inl : Eq (α := ℕ∞) (⨅ (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 : ℕ∞))

Tactic:
rw [h1, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Module.SpanRank
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) ⊤
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 : ℕ∞) ⊤
⊢ Eq (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M).card : ℕ∞)) ⊤

Tactic:
simp_rw [iInf_eq_top] at h1 ⊢

Premises used: iInf_eq_top
-- Module: Mathlib.Algebra.Module.SpanRank
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 : ∀ (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:
fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))

Premises used: Iff.mpr, False.elim, SetLike.coe, Finset.finite_toSet, Set.encard_ne_top_iff, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.SpanRank
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 : ∀ (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:
exact fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))

Premises used: Iff.mpr, False.elim, Set.encard_ne_top_iff
-- Module: Mathlib.Algebra.Module.SpanRank
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 :
  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)
⊢ 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:
simp_rw [← Set.encard_coe_eq_coe_finsetCard]

Premises used: Set.encard_coe_eq_coe_finsetCard
-- Module: Mathlib.Algebra.Module.SpanRank
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)
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)
⊢ 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:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.SpanRank
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 : 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:
le_iInf fun s ↦ iInf₂_le (s.1 : Set M) s.2

Premises used: iInf₂_le, le_iInf, SetLike.coe, Subtype.val
-- Module: Mathlib.Algebra.Module.SpanRank
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 : 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:
exact le_iInf fun s ↦ iInf₂_le (s.1 : Set M) s.2

Premises used: le_iInf
-- Module: Mathlib.Algebra.Module.SpanRank
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)

Tactic:
le_iInf fun s ↦ le_iInf fun h ↦ ?_

Premises used: le_iInf
-- Module: Mathlib.Algebra.Module.SpanRank
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 :
  ∀ (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
⊢ 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:
refine le_iInf fun s ↦ le_iInf fun h ↦ ?_

Premises used: le_iInf
-- Module: Mathlib.Algebra.Module.SpanRank
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
neg :
  ∀ (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

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ span R (↑(hs.toFinset (s := s)) : Set M) = p

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ (↑(↑(Subtype.mk (p := fun (s : Finset M) ↦ span R (↑s : Set M) = p) (hs.toFinset (s := s)) ⋯) : Finset M) :
        Set M).encard ≤
    s.encard

Tactic:
simp
-- Module: Mathlib.Algebra.Module.SpanRank
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

Tactic:
exact iInf_le_of_le ⟨hs.toFinset, by simpa⟩ (by simp)

Premises used: iInf_le_of_le
-- Module: Mathlib.Algebra.Module.SpanRank
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
neg : LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard) ⊤
⊢ ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard ≤ s.encard

Tactic:
rw [Set.Infinite.encard_eq hs]

Premises used: Set.Infinite.encard_eq
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard) ⊤

Tactic:
OrderTop.le_top _

Premises used: OrderTop.le_top
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ LE.le (α := ℕ∞) (⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑(↑s : Finset M) : Set M).encard) ⊤

Tactic:
exact OrderTop.le_top _

Premises used: OrderTop.le_top
-- Module: Mathlib.Algebra.Module.SpanRank
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.spanFinrank = ⨅ (s : { s : Finset M // span R (↑s : Set M) = p }), (↑s : Finset M).card

Tactic:
simp [spanFinrank, Cardinal.toNat, spanRank_toENat_eq_iInf_finset_card, ENat.iInf_toNat]

Premises used: ENat.iInf_toNat, Cardinal.toNat, Submodule.spanRank_toENat_eq_iInf_finset_card, Submodule.spanFinrank
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ ↔ ∃ (S : Set M), S.Finite ∧ span R S = p
⊢ p.spanRank < ℵ₀ ↔ p.FG

Tactic:
rw [spanRank, Submodule.fg_def]

Premises used: Submodule.fg_def, Submodule.spanRank
-- Module: Mathlib.Algebra.Module.SpanRank
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
mpr : (∃ (S : Set M), S.Finite ∧ span R S = p) → ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
⊢ ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀ ↔ ∃ (S : Set M), S.Finite ∧ span R S = p

Tactic:
constructor