R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
⊢ Set.Finite s
refine'
  by_contradiction fun hf =>
    (RelEmbedding.wellFounded_iff_no_descending_seq.1 (wellFounded_submodule_gt R M)).elim' _
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
have f : ℕ ↪ s := Set.Infinite.natEmbedding s hf
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
have : ∀ n, (↑) ∘ f '' { m | m ≤ n } ⊆ s := by
  rintro n x ⟨y, _, rfl⟩
  exact (f y).2
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
let coe' : s → M := (↑)
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
have : ∀ a b : ℕ, a ≤ b ↔
  span R (coe' ∘ f '' { m | m ≤ a }) ≤ span R ((↑) ∘ f '' { m | m ≤ b }) := by
  intro a b
  rw [span_le_span_iff hs (this a) (this b),
    Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective), Set.subset_def]
  exact ⟨fun hab x (hxa : x ≤ a) => le_trans hxa hab, fun hx => hx a (le_refl a)⟩
no goals
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
exact
  ⟨⟨fun n => span R (coe' ∘ f '' { m | m ≤ n }), fun x y => by
      rw [le_antisymm_iff, (this x y).symm, (this y x).symm, ←le_antisymm_iff, imp_self]
      trivial⟩,
    by dsimp [GT.gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
n y : ℕ
left✝ : y ∈ {m | m ≤ n}
⊢ (Subtype.val ∘ ↑f) y ∈ s
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
⊢ ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
rintro n x ⟨y, _, rfl⟩
no goals
case intro.intro
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
n y : ℕ
left✝ : y ∈ {m | m ≤ n}
⊢ (Subtype.val ∘ ↑f) y ∈ s
exact (f y).2
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
a b : ℕ
⊢ a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
⊢ ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
intro a b
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
a b : ℕ
⊢ a ≤ b ↔ ∀ (x : ℕ), x ∈ {m | m ≤ a} → x ∈ {m | m ≤ b}
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
a b : ℕ
⊢ a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
rw [span_le_span_iff hs (this a) (this b),
  Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective), Set.subset_def]
no goals
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
a b : ℕ
⊢ a ≤ b ↔ ∀ (x : ℕ), x ∈ {m | m ≤ a} → x ∈ {m | m ≤ b}
exact ⟨fun hab x (hxa : x ≤ a) => le_trans hxa hab, fun hx => hx a (le_refl a)⟩
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
x y : ℕ
⊢ True
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
x y : ℕ
⊢ (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) x = (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) y → x = y
rw [le_antisymm_iff, (this x y).symm, (this y x).symm, ←le_antisymm_iff, imp_self]
no goals
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
x y : ℕ
⊢ True
trivial
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ ∀ {a b : ℕ}, span R (Subtype.val ∘ ↑f '' {m | m ≤ b}) < span R (Subtype.val ∘ ↑f '' {m | m ≤ a}) ↔ b < a
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ ∀ {a b : ℕ},
    ↑{ toFun := fun n => span R (coe' ∘ ↑f '' {m | m ≤ n}),
              inj' :=
                (_ :
                  ∀ (x y : ℕ),
                    (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) x = (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) y →
                      x = y) }
          a >
        ↑{ toFun := fun n => span R (coe' ∘ ↑f '' {m | m ≤ n}),
              inj' :=
                (_ :
                  ∀ (x y : ℕ),
                    (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) x = (fun n => span R (coe' ∘ ↑f '' {m | m ≤ n})) y →
                      x = y) }
          b ↔
      a > b
dsimp [GT.gt]
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ ∀ {a b : ℕ}, True
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ ∀ {a b : ℕ}, span R (Subtype.val ∘ ↑f '' {m | m ≤ b}) < span R (Subtype.val ∘ ↑f '' {m | m ≤ a}) ↔ b < a
simp only [lt_iff_le_not_le, (this _ _).symm]
no goals
R : Type u_1
M : Type u_2
P : Type ?u.122472
N : Type w
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Nontrivial R
inst✝ : IsNoetherian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬Set.Finite s
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ↑f '' {m | m ≤ n} ⊆ s
coe' : ↑s → M := Subtype.val
this : ∀ (a b : ℕ), a ≤ b ↔ span R (coe' ∘ ↑f '' {m | m ≤ a}) ≤ span R (Subtype.val ∘ ↑f '' {m | m ≤ b})
⊢ ∀ {a b : ℕ}, True
tauto