R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
⊢ IsArtinian R { x // x ∈ N }
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
⊢ IsArtinian R { x // x ∈ N }
let ⟨s, hs⟩ := hN
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this : DecidableEq M
⊢ IsArtinian R { x // x ∈ N }
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
⊢ IsArtinian R { x // x ∈ N }
haveI := Classical.decEq M
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝ : DecidableEq M
this : DecidableEq R
⊢ IsArtinian R { x // x ∈ N }
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this : DecidableEq M
⊢ IsArtinian R { x // x ∈ N }
haveI := Classical.decEq R
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ IsArtinian R { x // x ∈ N }
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝ : DecidableEq M
this : DecidableEq R
⊢ IsArtinian R { x // x ∈ N }
have : ∀ x ∈ s, x ∈ N := fun x hx => hs ▸ Submodule.subset_span hx
case refine'_1
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ (↑↑s →₀ R) →ₗ[R] { x // x ∈ N }

case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑?refine'_1
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ IsArtinian R { x // x ∈ N }
refine' @isArtinian_of_surjective _ ((↑s : Set M) →₀ R) N _ _ _ _ _ _ _ isArtinian_finsupp
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑(Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) })
case refine'_1
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ (↑↑s →₀ R) →ₗ[R] { x // x ∈ N }

case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑?refine'_1
. exact Finsupp.total (↑s : Set M) N R (fun i => ⟨i, hs ▸ subset_span i.2⟩)
no goals
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑(Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) })
. rw [← LinearMap.range_eq_top, eq_top_iff,
     ← map_le_map_iff_of_injective (show Injective (Submodule.subtype N)
       from Subtype.val_injective), Submodule.map_top, range_subtype,
       ← Submodule.map_top, ← Submodule.map_comp, Submodule.map_top]
  subst N
  refine span_le.2 (fun i hi => ?_)
  use Finsupp.single ⟨i, hi⟩ 1
  simp
no goals
case refine'_1
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ (↑↑s →₀ R) →ₗ[R] { x // x ∈ N }
exact Finsupp.total (↑s : Set M) N R (fun i => ⟨i, hs ▸ subset_span i.2⟩)
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ N ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype N)
        (Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) }))
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ Surjective ↑(Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) })
rw [← LinearMap.range_eq_top, eq_top_iff,
   ← map_le_map_iff_of_injective (show Injective (Submodule.subtype N)
     from Subtype.val_injective), Submodule.map_top, range_subtype,
     ← Submodule.map_top, ← Submodule.map_comp, Submodule.map_top]
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
⊢ span R ↑s ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype (span R ↑s))
        (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝¹ : DecidableEq M
this✝ : DecidableEq R
this : ∀ (x : M), x ∈ s → x ∈ N
⊢ N ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype N)
        (Finsupp.total ↑↑s { x // x ∈ N } R fun i => { val := ↑i, property := (_ : ↑i ∈ N) }))
subst N
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ i ∈
    ↑(LinearMap.range
        (LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) })))
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
⊢ span R ↑s ≤
    LinearMap.range
      (LinearMap.comp (Submodule.subtype (span R ↑s))
        (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
refine span_le.2 (fun i hi => ?_)
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ ↑(LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
      (Finsupp.single { val := i, property := hi } 1) =
    i
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ i ∈
    ↑(LinearMap.range
        (LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) })))
use Finsupp.single ⟨i, hi⟩ 1
no goals
case refine'_2
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
s : Finset M
this✝¹ : DecidableEq M
this✝ : DecidableEq R
hN : FG (span R ↑s)
this : ∀ (x : M), x ∈ s → x ∈ span R ↑s
i : M
hi : i ∈ ↑s
⊢ ↑(LinearMap.comp (Submodule.subtype (span R ↑s))
          (Finsupp.total ↑↑s { x // x ∈ span R ↑s } R fun i => { val := ↑i, property := (_ : ↑i ∈ span R ↑s) }))
      (Finsupp.single { val := i, property := hi } 1) =
    i
simp