[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
⊢ IsNoetherian R { x // x ∈ N } ↔ ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
[PROOFSTEP]
refine
  ⟨fun ⟨hn⟩ => fun s hs =>
    have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
    Submodule.map_comap_eq_self this ▸ (hn _).map _,
    fun h => ⟨fun s => ?_⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
⊢ Submodule.FG s
[PROOFSTEP]
have f := (Submodule.equivMapOfInjective N.subtype Subtype.val_injective s).symm
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
⊢ Submodule.FG s
[PROOFSTEP]
have h₁ := h (s.map N.subtype) (Submodule.map_subtype_le N s)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
⊢ Submodule.FG s
[PROOFSTEP]
have h₂ : (⊤ : Submodule R (s.map N.subtype)).map f = ⊤ := by simp
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
⊢ Submodule.map f ⊤ = ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
⊢ Submodule.FG s
[PROOFSTEP]
have h₃ := ((Submodule.fg_top _).2 h₁).map (↑f : _ →ₗ[R] s)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
h₃ : Submodule.FG (Submodule.map ↑f ⊤)
⊢ Submodule.FG s
[PROOFSTEP]
exact (Submodule.fg_top _).1 (h₂ ▸ h₃)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
⊢ IsNoetherian R { x // x ∈ ⊤ } ↔ IsNoetherian R M
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
⊢ IsNoetherian R { x // x ∈ ⊤ } → IsNoetherian R M
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
⊢ IsNoetherian R M → IsNoetherian R { x // x ∈ ⊤ }
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R { x // x ∈ ⊤ }
⊢ IsNoetherian R M
[PROOFSTEP]
exact isNoetherian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl)
[GOAL]
case mpr
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R M
⊢ IsNoetherian R { x // x ∈ ⊤ }
[PROOFSTEP]
exact isNoetherian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl).symm
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
haveI := Classical.decEq ι
[GOAL]
case intro
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
suffices on_finset : ∀ s : Finset ι, IsNoetherian R (∀ i : s, M i)
[GOAL]
case intro
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
on_finset : ∀ (s : Finset ι), IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
let coe_e := Equiv.subtypeUnivEquiv <| @Finset.mem_univ ι _
[GOAL]
case intro
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
on_finset : ∀ (s : Finset ι), IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
coe_e : { x // x ∈ Finset.univ } ≃ ι := Equiv.subtypeUnivEquiv (_ : ∀ (x : ι), x ∈ Finset.univ)
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
letI : IsNoetherian R (∀ i : Finset.univ, M (coe_e i)) := on_finset Finset.univ
[GOAL]
case intro
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
on_finset : ∀ (s : Finset ι), IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
coe_e : { x // x ∈ Finset.univ } ≃ ι := Equiv.subtypeUnivEquiv (_ : ∀ (x : ι), x ∈ Finset.univ)
this : IsNoetherian R ((i : { x // x ∈ Finset.univ }) → M (↑coe_e i)) := on_finset Finset.univ
⊢ IsNoetherian R ((i : ι) → M i)
[PROOFSTEP]
exact isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R M coe_e)
[GOAL]
case on_finset
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
⊢ ∀ (s : Finset ι), IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
[PROOFSTEP]
intro s
[GOAL]
case on_finset
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
⊢ IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
[PROOFSTEP]
induction' s using Finset.induction with a s has ih
[GOAL]
case on_finset.empty
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
⊢ IsNoetherian R ((i : { x // x ∈ ∅ }) → M ↑i)
[PROOFSTEP]
exact
  ⟨fun s => by
    have : s = ⊥ := by simp only [eq_iff_true_of_subsingleton]
    rw [this]
    apply Submodule.fg_bot⟩
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Submodule R ((i : { x // x ∈ ∅ }) → M ↑i)
⊢ Submodule.FG s
[PROOFSTEP]
have : s = ⊥ := by simp only [eq_iff_true_of_subsingleton]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Submodule R ((i : { x // x ∈ ∅ }) → M ↑i)
⊢ s = ⊥
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
s : Submodule R ((i : { x // x ∈ ∅ }) → M ↑i)
this : s = ⊥
⊢ Submodule.FG s
[PROOFSTEP]
rw [this]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
s : Submodule R ((i : { x // x ∈ ∅ }) → M ↑i)
this : s = ⊥
⊢ Submodule.FG ⊥
[PROOFSTEP]
apply Submodule.fg_bot
[GOAL]
case on_finset.insert
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ IsNoetherian R ((i : { x // x ∈ insert a s }) → M ↑i)
[PROOFSTEP]
refine
  @isNoetherian_of_linearEquiv R (M a × ((i : s) → M i)) _ _ _ _ _ _ ?_ <| @isNoetherian_prod R (M a) _ _ _ _ _ _ _ ih
[GOAL]
case on_finset.insert
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ (M a × ((i : { x // x ∈ s }) → M ↑i)) ≃ₗ[R] (i : { x // x ∈ insert a s }) → M ↑i
[PROOFSTEP]
refine
  { toFun := fun f i =>
      (Finset.mem_insert.1 i.2).by_cases (fun h : i.1 = a => show M i.1 from Eq.recOn h.symm f.1)
        (fun h : i.1 ∈ s => show M i.1 from f.2 ⟨i.1, h⟩),
    invFun := fun f => (f ⟨a, Finset.mem_insert_self _ _⟩, fun i => f ⟨i.1, Finset.mem_insert_of_mem i.2⟩),
    map_add' := ?_, map_smul' := ?_
    left_inv := ?_, right_inv := ?_ }
[GOAL]
case on_finset.insert.refine_1
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ ∀ (x y : M a × ((i : { x // x ∈ s }) → M ↑i)),
    (fun f i =>
          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
            (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            fun h =>
            let_fun this := Prod.snd f { val := ↑i, property := h };
            this)
        (x + y) =
      (fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
          x +
        (fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
          y
[PROOFSTEP]
intro f g
[GOAL]
case on_finset.insert.refine_1
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
⊢ (fun f i =>
        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
          (fun h =>
            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
            this)
          fun h =>
          let_fun this := Prod.snd f { val := ↑i, property := h };
          this)
      (f + g) =
    (fun f i =>
          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
            (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            fun h =>
            let_fun this := Prod.snd f { val := ↑i, property := h };
            this)
        f +
      (fun f i =>
          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
            (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            fun h =>
            let_fun this := Prod.snd f { val := ↑i, property := h };
            this)
        g
[PROOFSTEP]
ext i
[GOAL]
case on_finset.insert.refine_1.h
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : { x // x ∈ insert a s }
⊢ (fun f i =>
        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
          (fun h =>
            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
            this)
          fun h =>
          let_fun this := Prod.snd f { val := ↑i, property := h };
          this)
      (f + g) i =
    ((fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
          f +
        (fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
          g)
      i
[PROOFSTEP]
unfold Or.by_cases
[GOAL]
case on_finset.insert.refine_1.h
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : { x // x ∈ insert a s }
⊢ (fun f i =>
        if hp : ↑i = a then
          (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
            (_ : ↑i ∈ s))
      (f + g) i =
    ((fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          f +
        (fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          g)
      i
[PROOFSTEP]
cases' i with i hi
[GOAL]
case on_finset.insert.refine_1.h.mk
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
⊢ (fun f i =>
        if hp : ↑i = a then
          (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
            (_ : ↑i ∈ s))
      (f + g) { val := i, property := hi } =
    ((fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          f +
        (fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          g)
      { val := i, property := hi }
[PROOFSTEP]
rcases Finset.mem_insert.1 hi with (rfl | h)
[GOAL]
case on_finset.insert.refine_1.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
has : ¬i ∈ s
f g : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ (fun f i_1 =>
        if hp : ↑i_1 = i then
          (fun h =>
              let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i_1, property := h };
              this)
            (_ : ↑i_1 ∈ s))
      (f + g) { val := i, property := hi } =
    ((fun f i_1 =>
            if hp : ↑i_1 = i then
              (fun h =>
                  let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i_1, property := h };
                  this)
                (_ : ↑i_1 ∈ s))
          f +
        (fun f i_1 =>
            if hp : ↑i_1 = i then
              (fun h =>
                  let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i_1, property := h };
                  this)
                (_ : ↑i_1 ∈ s))
          g)
      { val := i, property := hi }
[PROOFSTEP]
change _ = _ + _
[GOAL]
case on_finset.insert.refine_1.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
has : ¬i ∈ s
f g : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ (fun f i_1 =>
        if hp : ↑i_1 = i then
          (fun h =>
              let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i_1, property := h };
              this)
            (_ : ↑i_1 ∈ s))
      (f + g) { val := i, property := hi } =
    (fun f i_1 =>
          if hp : ↑i_1 = i then
            (fun h =>
                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i_1, property := h };
                this)
              (_ : ↑i_1 ∈ s))
        f { val := i, property := hi } +
      (fun f i_1 =>
          if hp : ↑i_1 = i then
            (fun h =>
                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i_1, property := h };
                this)
              (_ : ↑i_1 ∈ s))
        g { val := i, property := hi }
[PROOFSTEP]
simp only [dif_pos]
[GOAL]
case on_finset.insert.refine_1.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
has : ¬i ∈ s
f g : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ (f + g).fst = f.fst + g.fst
[PROOFSTEP]
rfl
[GOAL]
case on_finset.insert.refine_1.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ (fun f i =>
        if hp : ↑i = a then
          (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
            (_ : ↑i ∈ s))
      (f + g) { val := i, property := hi } =
    ((fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          f +
        (fun f i =>
            if hp : ↑i = a then
              (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                hp
            else
              (fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this)
                (_ : ↑i ∈ s))
          g)
      { val := i, property := hi }
[PROOFSTEP]
change _ = _ + _
[GOAL]
case on_finset.insert.refine_1.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ (fun f i =>
        if hp : ↑i = a then
          (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
            (_ : ↑i ∈ s))
      (f + g) { val := i, property := hi } =
    (fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s))
        f { val := i, property := hi } +
      (fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s))
        g { val := i, property := hi }
[PROOFSTEP]
have : ¬i = a := by
  rintro rfl
  exact has h
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ ¬i = a
[PROOFSTEP]
rintro rfl
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
h : i ∈ s
has : ¬i ∈ s
f g : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ False
[PROOFSTEP]
exact has h
[GOAL]
case on_finset.insert.refine_1.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
this : ¬i = a
⊢ (fun f i =>
        if hp : ↑i = a then
          (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            hp
        else
          (fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this)
            (_ : ↑i ∈ s))
      (f + g) { val := i, property := hi } =
    (fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s))
        f { val := i, property := hi } +
      (fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s))
        g { val := i, property := hi }
[PROOFSTEP]
simp only [dif_neg this, dif_pos h]
[GOAL]
case on_finset.insert.refine_1.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f g : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
this : ¬i = a
⊢ Prod.snd (f + g) { val := i, property := (_ : i ∈ s) } =
    Prod.snd f { val := i, property := (_ : i ∈ s) } + Prod.snd g { val := i, property := (_ : i ∈ s) }
[PROOFSTEP]
rfl
[GOAL]
case on_finset.insert.refine_2
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ ∀ (r : R) (x : M a × ((i : { x // x ∈ s }) → M ↑i)),
    AddHom.toFun
        {
          toFun := fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this,
          map_add' :=
            (_ :
              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    (f + g) =
                  (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      f +
                    (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      g) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun := fun f i =>
              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this,
            map_add' :=
              (_ :
                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      (f + g) =
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        f +
                      (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        g) }
          x
[PROOFSTEP]
intro c f
[GOAL]
case on_finset.insert.refine_2
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
⊢ AddHom.toFun
      {
        toFun := fun f i =>
          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
            (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            fun h =>
            let_fun this := Prod.snd f { val := ↑i, property := h };
            this,
        map_add' :=
          (_ :
            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this)
                  (f + g) =
                (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    f +
                  (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    g) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        {
          toFun := fun f i =>
            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
              (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              fun h =>
              let_fun this := Prod.snd f { val := ↑i, property := h };
              this,
          map_add' :=
            (_ :
              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    (f + g) =
                  (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      f +
                    (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      g) }
        f
[PROOFSTEP]
ext i
[GOAL]
case on_finset.insert.refine_2.h
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : { x // x ∈ insert a s }
⊢ AddHom.toFun
      {
        toFun := fun f i =>
          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
            (fun h =>
              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
              this)
            fun h =>
            let_fun this := Prod.snd f { val := ↑i, property := h };
            this,
        map_add' :=
          (_ :
            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this)
                  (f + g) =
                (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    f +
                  (fun f i =>
                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                        (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        fun h =>
                        let_fun this := Prod.snd f { val := ↑i, property := h };
                        this)
                    g) }
      (c • f) i =
    (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f i =>
              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                (fun h =>
                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                  this)
                fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this,
            map_add' :=
              (_ :
                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                      (f + g) =
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        f +
                      (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        g) }
          f)
      i
[PROOFSTEP]
unfold Or.by_cases
[GOAL]
case on_finset.insert.refine_2.h
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : { x // x ∈ insert a s }
⊢ AddHom.toFun
      {
        toFun := fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s),
        map_add' :=
          (_ :
            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i =>
                    if hp : ↑i = a then
                      (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        hp
                    else
                      (fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                        (_ : ↑i ∈ s))
                  (f + g) =
                (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    f +
                  (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    g) }
      (c • f) i =
    (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f i =>
              if hp : ↑i = a then
                (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  hp
              else
                (fun h =>
                    let_fun this := Prod.snd f { val := ↑i, property := h };
                    this)
                  (_ : ↑i ∈ s),
            map_add' :=
              (_ :
                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i =>
                        if hp : ↑i = a then
                          (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            hp
                        else
                          (fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                            (_ : ↑i ∈ s))
                      (f + g) =
                    (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        f +
                      (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        g) }
          f)
      i
[PROOFSTEP]
cases' i with i hi
[GOAL]
case on_finset.insert.refine_2.h.mk
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
⊢ AddHom.toFun
      {
        toFun := fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s),
        map_add' :=
          (_ :
            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i =>
                    if hp : ↑i = a then
                      (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        hp
                    else
                      (fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                        (_ : ↑i ∈ s))
                  (f + g) =
                (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    f +
                  (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    g) }
      (c • f) { val := i, property := hi } =
    (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f i =>
              if hp : ↑i = a then
                (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  hp
              else
                (fun h =>
                    let_fun this := Prod.snd f { val := ↑i, property := h };
                    this)
                  (_ : ↑i ∈ s),
            map_add' :=
              (_ :
                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i =>
                        if hp : ↑i = a then
                          (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            hp
                        else
                          (fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                            (_ : ↑i ∈ s))
                      (f + g) =
                    (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        f +
                      (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        g) }
          f)
      { val := i, property := hi }
[PROOFSTEP]
rcases Finset.mem_insert.1 hi with (rfl | h)
[GOAL]
case on_finset.insert.refine_2.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
i : ι
has : ¬i ∈ s
f : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ AddHom.toFun
      {
        toFun := fun f i_1 =>
          if hp : ↑i_1 = i then
            (fun h =>
                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i_1, property := h };
                this)
              (_ : ↑i_1 ∈ s),
        map_add' :=
          (_ :
            ∀ (f g : M i × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i_1 =>
                    if hp : ↑i_1 = i then
                      (fun h =>
                          let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                          this)
                        hp
                    else
                      (fun h =>
                          let_fun this := Prod.snd f { val := ↑i_1, property := h };
                          this)
                        (_ : ↑i_1 ∈ s))
                  (f + g) =
                (fun f i_1 =>
                      if hp : ↑i_1 = i then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i_1, property := h };
                            this)
                          (_ : ↑i_1 ∈ s))
                    f +
                  (fun f i_1 =>
                      if hp : ↑i_1 = i then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i_1, property := h };
                            this)
                          (_ : ↑i_1 ∈ s))
                    g) }
      (c • f) { val := i, property := hi } =
    (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f i_1 =>
              if hp : ↑i_1 = i then
                (fun h =>
                    let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                    this)
                  hp
              else
                (fun h =>
                    let_fun this := Prod.snd f { val := ↑i_1, property := h };
                    this)
                  (_ : ↑i_1 ∈ s),
            map_add' :=
              (_ :
                ∀ (f g : M i × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i_1 =>
                        if hp : ↑i_1 = i then
                          (fun h =>
                              let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                              this)
                            hp
                        else
                          (fun h =>
                              let_fun this := Prod.snd f { val := ↑i_1, property := h };
                              this)
                            (_ : ↑i_1 ∈ s))
                      (f + g) =
                    (fun f i_1 =>
                          if hp : ↑i_1 = i then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                this)
                              (_ : ↑i_1 ∈ s))
                        f +
                      (fun f i_1 =>
                          if hp : ↑i_1 = i then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                this)
                              (_ : ↑i_1 ∈ s))
                        g) }
          f)
      { val := i, property := hi }
[PROOFSTEP]
dsimp
[GOAL]
case on_finset.insert.refine_2.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
i : ι
has : ¬i ∈ s
f : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ (if hp : i = i then c • f.fst else c • Prod.snd f { val := i, property := (_ : i ∈ s) }) =
    c • if hp : i = i then f.fst else Prod.snd f { val := i, property := (_ : i ∈ s) }
[PROOFSTEP]
simp only [dif_pos]
[GOAL]
case on_finset.insert.refine_2.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ AddHom.toFun
      {
        toFun := fun f i =>
          if hp : ↑i = a then
            (fun h =>
                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                this)
              hp
          else
            (fun h =>
                let_fun this := Prod.snd f { val := ↑i, property := h };
                this)
              (_ : ↑i ∈ s),
        map_add' :=
          (_ :
            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
              (fun f i =>
                    if hp : ↑i = a then
                      (fun h =>
                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                          this)
                        hp
                    else
                      (fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this)
                        (_ : ↑i ∈ s))
                  (f + g) =
                (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    f +
                  (fun f i =>
                      if hp : ↑i = a then
                        (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          hp
                      else
                        (fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                          (_ : ↑i ∈ s))
                    g) }
      (c • f) { val := i, property := hi } =
    (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f i =>
              if hp : ↑i = a then
                (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  hp
              else
                (fun h =>
                    let_fun this := Prod.snd f { val := ↑i, property := h };
                    this)
                  (_ : ↑i ∈ s),
            map_add' :=
              (_ :
                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  (fun f i =>
                        if hp : ↑i = a then
                          (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            hp
                        else
                          (fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                            (_ : ↑i ∈ s))
                      (f + g) =
                    (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        f +
                      (fun f i =>
                          if hp : ↑i = a then
                            (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              hp
                          else
                            (fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                              (_ : ↑i ∈ s))
                        g) }
          f)
      { val := i, property := hi }
[PROOFSTEP]
dsimp
[GOAL]
case on_finset.insert.refine_2.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ (if hp : i = a then (_ : a = i) ▸ (c • f.fst) else c • Prod.snd f { val := i, property := (_ : i ∈ s) }) =
    c • if hp : i = a then (_ : a = i) ▸ f.fst else Prod.snd f { val := i, property := (_ : i ∈ s) }
[PROOFSTEP]
have : ¬i = a := by
  rintro rfl
  exact has h
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ ¬i = a
[PROOFSTEP]
rintro rfl
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
i : ι
h : i ∈ s
has : ¬i ∈ s
f : M i × ((i : { x // x ∈ s }) → M ↑i)
hi : i ∈ insert i s
⊢ False
[PROOFSTEP]
exact has h
[GOAL]
case on_finset.insert.refine_2.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
c : R
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
hi : i ∈ insert a s
h : i ∈ s
this : ¬i = a
⊢ (if hp : i = a then (_ : a = i) ▸ (c • f.fst) else c • Prod.snd f { val := i, property := (_ : i ∈ s) }) =
    c • if hp : i = a then (_ : a = i) ▸ f.fst else Prod.snd f { val := i, property := (_ : i ∈ s) }
[PROOFSTEP]
simp only [dif_neg this, dif_pos h]
[GOAL]
case on_finset.insert.refine_3
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ Function.LeftInverse
    (fun f =>
      (f { val := a, property := (_ : a ∈ insert a s) }, fun i => f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
    {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom.toFun
[PROOFSTEP]
intro f
[GOAL]
case on_finset.insert.refine_3
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
⊢ (fun f =>
        (f { val := a, property := (_ : a ∈ insert a s) }, fun i => f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
      (AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun f i =>
                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                    (fun h =>
                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                      this)
                    fun h =>
                    let_fun this := Prod.snd f { val := ↑i, property := h };
                    this,
                map_add' :=
                  (_ :
                    ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          (f + g) =
                        (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            f +
                          (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            g) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                  AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this,
                          map_add' :=
                            (_ :
                              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    (f + g) =
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      f +
                                    (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      g) }
                        f) }.toAddHom
        f) =
    f
[PROOFSTEP]
apply Prod.ext
[GOAL]
case on_finset.insert.refine_3.h₁
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
⊢ ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        (AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this,
                  map_add' :=
                    (_ :
                      ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                        (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            (f + g) =
                          (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              f +
                            (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              g) },
              map_smul' :=
                (_ :
                  ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    AddHom.toFun
                        {
                          toFun := fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this,
                          map_add' :=
                            (_ :
                              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    (f + g) =
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      f +
                                    (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      g) }
                        (c • f) =
                      ↑(RingHom.id R) c •
                        AddHom.toFun
                          {
                            toFun := fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this,
                            map_add' :=
                              (_ :
                                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      (f + g) =
                                    (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        f +
                                      (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        g) }
                          f) }.toAddHom
          f)).fst =
    f.fst
[PROOFSTEP]
simp only [Or.by_cases, dif_pos]
[GOAL]
case on_finset.insert.refine_3.h₂
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
⊢ ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        (AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this,
                  map_add' :=
                    (_ :
                      ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                        (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            (f + g) =
                          (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              f +
                            (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              g) },
              map_smul' :=
                (_ :
                  ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    AddHom.toFun
                        {
                          toFun := fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this,
                          map_add' :=
                            (_ :
                              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    (f + g) =
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      f +
                                    (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      g) }
                        (c • f) =
                      ↑(RingHom.id R) c •
                        AddHom.toFun
                          {
                            toFun := fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this,
                            map_add' :=
                              (_ :
                                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      (f + g) =
                                    (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        f +
                                      (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        g) }
                          f) }.toAddHom
          f)).snd =
    f.snd
[PROOFSTEP]
ext ⟨i, his⟩
[GOAL]
case on_finset.insert.refine_3.h₂.h.mk
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
his : i ∈ s
⊢ Prod.snd
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        (AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this,
                  map_add' :=
                    (_ :
                      ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                        (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            (f + g) =
                          (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              f +
                            (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              g) },
              map_smul' :=
                (_ :
                  ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    AddHom.toFun
                        {
                          toFun := fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this,
                          map_add' :=
                            (_ :
                              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    (f + g) =
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      f +
                                    (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      g) }
                        (c • f) =
                      ↑(RingHom.id R) c •
                        AddHom.toFun
                          {
                            toFun := fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this,
                            map_add' :=
                              (_ :
                                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      (f + g) =
                                    (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        f +
                                      (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        g) }
                          f) }.toAddHom
          f))
      { val := i, property := his } =
    Prod.snd f { val := i, property := his }
[PROOFSTEP]
have : ¬i = a := by
  rintro rfl
  exact has his
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
his : i ∈ s
⊢ ¬i = a
[PROOFSTEP]
rintro rfl
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
his : i ∈ s
has : ¬i ∈ s
f : M i × ((i : { x // x ∈ s }) → M ↑i)
⊢ False
[PROOFSTEP]
exact has his
[GOAL]
case on_finset.insert.refine_3.h₂.h.mk
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : M a × ((i : { x // x ∈ s }) → M ↑i)
i : ι
his : i ∈ s
this : ¬i = a
⊢ Prod.snd
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        (AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun f i =>
                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                      (fun h =>
                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                        this)
                      fun h =>
                      let_fun this := Prod.snd f { val := ↑i, property := h };
                      this,
                  map_add' :=
                    (_ :
                      ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                        (fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this)
                            (f + g) =
                          (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              f +
                            (fun f i =>
                                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                  (fun h =>
                                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                    this)
                                  fun h =>
                                  let_fun this := Prod.snd f { val := ↑i, property := h };
                                  this)
                              g) },
              map_smul' :=
                (_ :
                  ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    AddHom.toFun
                        {
                          toFun := fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this,
                          map_add' :=
                            (_ :
                              ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    (f + g) =
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      f +
                                    (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      g) }
                        (c • f) =
                      ↑(RingHom.id R) c •
                        AddHom.toFun
                          {
                            toFun := fun f i =>
                              Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                (fun h =>
                                  let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                  this)
                                fun h =>
                                let_fun this := Prod.snd f { val := ↑i, property := h };
                                this,
                            map_add' :=
                              (_ :
                                ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                                  (fun f i =>
                                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                          (fun h =>
                                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                            this)
                                          fun h =>
                                          let_fun this := Prod.snd f { val := ↑i, property := h };
                                          this)
                                      (f + g) =
                                    (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        f +
                                      (fun f i =>
                                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                            (fun h =>
                                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                              this)
                                            fun h =>
                                            let_fun this := Prod.snd f { val := ↑i, property := h };
                                            this)
                                        g) }
                          f) }.toAddHom
          f))
      { val := i, property := his } =
    Prod.snd f { val := i, property := his }
[PROOFSTEP]
simp only [Or.by_cases, this, not_false_iff, dif_neg]
[GOAL]
case on_finset.insert.refine_4
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
⊢ Function.RightInverse
    (fun f =>
      (f { val := a, property := (_ : a ∈ insert a s) }, fun i => f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
    {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom.toFun
[PROOFSTEP]
intro f
[GOAL]
case on_finset.insert.refine_4
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : (i : { x // x ∈ insert a s }) → M ↑i
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        f) =
    f
[PROOFSTEP]
ext ⟨i, hi⟩
[GOAL]
case on_finset.insert.refine_4.h.mk
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : (i : { x // x ∈ insert a s }) → M ↑i
i : ι
hi : i ∈ insert a s
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        f)
      { val := i, property := hi } =
    f { val := i, property := hi }
[PROOFSTEP]
rcases Finset.mem_insert.1 hi with (rfl | h)
[GOAL]
case on_finset.insert.refine_4.h.mk.inl
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
has : ¬i ∈ s
f : (i_1 : { x // x ∈ insert i s }) → M ↑i_1
hi : i ∈ insert i s
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f i_1 =>
                Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i_1, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M i × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i_1 =>
                          Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i_1, property := h };
                            this)
                        (f + g) =
                      (fun f i_1 =>
                            Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i_1, property := h };
                              this)
                          f +
                        (fun f i_1 =>
                            Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i_1, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M i × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i_1 =>
                        Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i_1, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M i × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i_1 =>
                                  Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                    this)
                                (f + g) =
                              (fun f i_1 =>
                                    Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                      this)
                                  f +
                                (fun f i_1 =>
                                    Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i_1 =>
                          Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i_1, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M i × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i_1 =>
                                    Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                      this)
                                  (f + g) =
                                (fun f i_1 =>
                                      Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                        this)
                                    f +
                                  (fun f i_1 =>
                                      Or.by_cases (_ : ↑i_1 = i ∨ ↑i_1 ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : i = ↑i_1) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i_1, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom
      ((fun f =>
          (f { val := i, property := (_ : i ∈ insert i s) }, fun i_1 =>
            f { val := ↑i_1, property := (_ : ↑i_1 ∈ insert i s) }))
        f)
      { val := i, property := hi } =
    f { val := i, property := hi }
[PROOFSTEP]
simp only [Or.by_cases, dif_pos]
[GOAL]
case on_finset.insert.refine_4.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : (i : { x // x ∈ insert a s }) → M ↑i
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        f)
      { val := i, property := hi } =
    f { val := i, property := hi }
[PROOFSTEP]
have : ¬i = a := by
  rintro rfl
  exact has h
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : (i : { x // x ∈ insert a s }) → M ↑i
i : ι
hi : i ∈ insert a s
h : i ∈ s
⊢ ¬i = a
[PROOFSTEP]
rintro rfl
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this : DecidableEq ι
s : Finset ι
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
i : ι
h : i ∈ s
has : ¬i ∈ s
f : (i_1 : { x // x ∈ insert i s }) → M ↑i_1
hi : i ∈ insert i s
⊢ False
[PROOFSTEP]
exact has h
[GOAL]
case on_finset.insert.refine_4.h.mk.inr
R✝ : Type u_1
M✝ : Type u_2
P : Type u_3
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ P
R : Type u_4
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Ring R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsNoetherian R (M i)
val✝ : Fintype ι
this✝ : DecidableEq ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih : IsNoetherian R ((i : { x // x ∈ s }) → M ↑i)
f : (i : { x // x ∈ insert a s }) → M ↑i
i : ι
hi : i ∈ insert a s
h : i ∈ s
this : ¬i = a
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f i =>
                Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                  (fun h =>
                    let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                    this)
                  fun h =>
                  let_fun this := Prod.snd f { val := ↑i, property := h };
                  this,
              map_add' :=
                (_ :
                  ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                    (fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this)
                        (f + g) =
                      (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          f +
                        (fun f i =>
                            Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                              (fun h =>
                                let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                this)
                              fun h =>
                              let_fun this := Prod.snd f { val := ↑i, property := h };
                              this)
                          g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : M a × ((i : { x // x ∈ s }) → M ↑i)),
                AddHom.toFun
                    {
                      toFun := fun f i =>
                        Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                          (fun h =>
                            let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                            this)
                          fun h =>
                          let_fun this := Prod.snd f { val := ↑i, property := h };
                          this,
                      map_add' :=
                        (_ :
                          ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                            (fun f i =>
                                  Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                    (fun h =>
                                      let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                      this)
                                    fun h =>
                                    let_fun this := Prod.snd f { val := ↑i, property := h };
                                    this)
                                (f + g) =
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  f +
                                (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun f i =>
                          Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                            (fun h =>
                              let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                              this)
                            fun h =>
                            let_fun this := Prod.snd f { val := ↑i, property := h };
                            this,
                        map_add' :=
                          (_ :
                            ∀ (f g : M a × ((i : { x // x ∈ s }) → M ↑i)),
                              (fun f i =>
                                    Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                      (fun h =>
                                        let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                        this)
                                      fun h =>
                                      let_fun this := Prod.snd f { val := ↑i, property := h };
                                      this)
                                  (f + g) =
                                (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    f +
                                  (fun f i =>
                                      Or.by_cases (_ : ↑i = a ∨ ↑i ∈ s)
                                        (fun h =>
                                          let_fun this := Eq.recOn (_ : a = ↑i) f.fst;
                                          this)
                                        fun h =>
                                        let_fun this := Prod.snd f { val := ↑i, property := h };
                                        this)
                                    g) }
                      f) }.toAddHom
      ((fun f =>
          (f { val := a, property := (_ : a ∈ insert a s) }, fun i =>
            f { val := ↑i, property := (_ : ↑i ∈ insert a s) }))
        f)
      { val := i, property := hi } =
    f { val := i, property := hi }
[PROOFSTEP]
simp only [Or.by_cases, dif_neg this, dif_pos h]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
have :=
  (CompleteLattice.wellFounded_characterisations <| Submodule R M).out 0
    3
      -- Porting note: inlining this makes rw complain about it being a metavariable
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
this : (WellFounded fun x x_1 => x > x_1) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
this : (WellFounded fun x x_1 => x > x_1) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
[PROOFSTEP]
exact ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h => ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
let α := { N : Submodule R M // N.FG }
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
⊢ IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
⊢ IsNoetherian R M → WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : IsNoetherian R M
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
let f : α ↪o Submodule R M := OrderEmbedding.subtype _
[GOAL]
case mp
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun N => FG N
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded f.dual (isNoetherian_iff_wellFounded.mp H)
[GOAL]
case mpr
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
⊢ (WellFounded fun x x_1 => x > x_1) → IsNoetherian R M
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
⊢ IsNoetherian R M
[PROOFSTEP]
constructor
[GOAL]
case mpr.noetherian
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
⊢ ∀ (s : Submodule R M), FG s
[PROOFSTEP]
intro N
[GOAL]
case mpr.noetherian
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N : Submodule R M
⊢ FG N
[PROOFSTEP]
obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ := WellFounded.has_min H {N' : α | N'.1 ≤ N} ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩
[GOAL]
case mpr.noetherian.intro.mk.intro
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
⊢ FG N
[PROOFSTEP]
convert h₁
[GOAL]
case h.e'_6
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
⊢ N = N₀
[PROOFSTEP]
refine' (e.antisymm _).symm
[GOAL]
case h.e'_6
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
⊢ N ≤ N₀
[PROOFSTEP]
by_contra h₃
[GOAL]
case h.e'_6
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
h₃ : ¬N ≤ N₀
⊢ False
[PROOFSTEP]
obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
[GOAL]
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : ¬x ∈ N₀
⊢ False
[PROOFSTEP]
apply hx₂
[GOAL]
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : ¬x ∈ N₀
⊢ x ∈ N₀
[PROOFSTEP]
rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _)
    (h₂ ⟨_, Submodule.FG.sup ⟨{ x }, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : ¬x ∈ N₀
⊢ span R ↑{x} = span R {x}
[PROOFSTEP]
rw [Finset.coe_singleton]
[GOAL]
case h.e'_6.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
N✝ : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N✝
inst✝² : Module R N✝
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_2 := { N // FG N }
H : WellFounded fun x x_1 => x > x_1
N N₀ : Submodule R M
h₁ : FG N₀
e : N₀ ≤ N
h₂ : ∀ (x : { N // FG N }), x ∈ {N' | ↑N' ≤ N} → ¬x > { val := N₀, property := h₁ }
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : ¬x ∈ N₀
⊢ x ∈ span R {x} ⊔ N₀
[PROOFSTEP]
exact (le_sup_left : (R ∙ x) ≤ _) (Submodule.mem_span_singleton_self _)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∀ (a : Set (Submodule R M)), Set.Nonempty a → ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), I ∈ a → ¬M' < I) ↔
    IsNoetherian R M
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded, WellFounded.wellFounded_iff_has_min]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ IsNoetherian R M
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
refine'
  by_contradiction fun hf => (RelEmbedding.wellFounded_iff_no_descending_seq.1 (wellFounded_submodule_gt R M)).elim' _
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
have f : ℕ ↪ s := Set.Infinite.natEmbedding s hf
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
have : ∀ n, (↑) ∘ f '' {m | m ≤ n} ⊆ s := by
  rintro n x ⟨y, _, rfl⟩
  exact (f y).2
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
rintro n x ⟨y, _, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
exact (f y).2
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
let coe' : s → M := (↑)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
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)⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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})
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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})
[PROOFSTEP]
rw [span_le_span_iff hs (this a) (this b), Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective),
  Set.subset_def]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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}
[PROOFSTEP]
exact ⟨fun hab x (hxa : x ≤ a) => le_trans hxa hab, fun hx => hx a (le_refl a)⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
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⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
rw [le_antisymm_iff, (this x y).symm, (this y x).symm, ← le_antisymm_iff, imp_self]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
trivial
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
dsimp [GT.gt]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
simp only [lt_iff_le_not_le, (this _ _).symm]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
[PROOFSTEP]
tauto
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Injective ↑f
hg : Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), map f (comap f a) = a ⊓ LinearMap.range f
[PROOFSTEP]
simp [Submodule.map_comap_eq, inf_comm]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Injective ↑f
hg : Surjective ↑g
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), comap g (map g a) = a ⊔ LinearMap.range f
[PROOFSTEP]
simp [Submodule.comap_map_eq, h]
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
[PROOFSTEP]
obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr I (f.iterateKer.comp ⟨fun n => n + 1, fun n m w => by linarith⟩)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n m : ℕ
w : n ≤ m
⊢ (fun n => n + 1) n ≤ (fun n => n + 1) m
[PROOFSTEP]
linarith
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateKer f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          n =
        ↑(OrderHom.comp (LinearMap.iterateKer f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          m
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
[PROOFSTEP]
specialize w (2 * n + 1) (by linarith only)
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      ↑(OrderHom.comp (LinearMap.iterateKer f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          n =
        ↑(OrderHom.comp (LinearMap.iterateKer f)
              { toFun := fun n => n + 1,
                monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
          m
⊢ n ≤ 2 * n + 1
[PROOFSTEP]
linarith only
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w :
  ↑(OrderHom.comp (LinearMap.iterateKer f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      n =
    ↑(OrderHom.comp (LinearMap.iterateKer f)
          { toFun := fun n => n + 1, monotone' := (_ : ∀ (n m : ℕ), n ≤ m → (fun n => n + 1) n ≤ (fun n => n + 1) m) })
      (2 * n + 1)
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
[PROOFSTEP]
dsimp at w
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
[PROOFSTEP]
refine' ⟨n + 1, Nat.succ_ne_zero _, _⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
⊢ LinearMap.ker (f ^ (n + 1)) ⊓ LinearMap.range (f ^ (n + 1)) ≤ ⊥
[PROOFSTEP]
rintro - ⟨h, ⟨y, rfl⟩⟩
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ ↑(f ^ (n + 1)) y ∈ ⊥
[PROOFSTEP]
rw [mem_bot, ← LinearMap.mem_ker, w]
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) y ∈ ↑(LinearMap.ker (f ^ (n + 1)))
⊢ y ∈ LinearMap.ker (f ^ (2 * n + 1 + 1))
[PROOFSTEP]
erw [LinearMap.mem_ker] at h ⊢
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1)) (↑(f ^ (n + 1)) y) = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
[PROOFSTEP]
change (f ^ (n + 1) * f ^ (n + 1)) y = 0 at h
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1) * f ^ (n + 1)) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
[PROOFSTEP]
rw [← pow_add] at h
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ ↑(f ^ (2 * n + 1 + 1)) y = 0
[PROOFSTEP]
convert h using 3
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
w : LinearMap.ker (f ^ (n + 1)) = LinearMap.ker (f ^ (2 * n + 1 + 1))
y : M
h : ↑(f ^ (n + 1 + (n + 1))) y = 0
⊢ 2 * n + 1 + 1 = n + 1 + (n + 1)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
⊢ Injective ↑f
[PROOFSTEP]
obtain ⟨n, ne, w⟩ := IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot f
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊓ LinearMap.range (f ^ n) = ⊥
⊢ Injective ↑f
[PROOFSTEP]
rw [LinearMap.range_eq_top.mpr (LinearMap.iterate_surjective s n), inf_top_eq, LinearMap.ker_eq_bot] at w
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective ↑f
n : ℕ
ne : n ≠ 0
w : Injective ↑(f ^ n)
⊢ Injective ↑f
[PROOFSTEP]
exact LinearMap.injective_of_iterate_injective ne w
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
[PROOFSTEP]
suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
t : ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
[PROOFSTEP]
obtain ⟨n, w⟩ := t
[GOAL]
case intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
[PROOFSTEP]
use n + 1
[GOAL]
case h
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∀ (m : ℕ), n + 1 ≤ m → f m = ⊥
[PROOFSTEP]
rintro (_ | m) p
[GOAL]
case h.zero
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ Nat.zero
⊢ f Nat.zero = ⊥
[PROOFSTEP]
cases p
[GOAL]
case h.succ
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ f (Nat.succ m) = ⊥
[PROOFSTEP]
apply w
[GOAL]
case h.succ.a
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ Nat.succ m
⊢ n ≤ m
[PROOFSTEP]
exact Nat.succ_le_succ_iff.mp p
[GOAL]
case t
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
[PROOFSTEP]
obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr I (partialSups f)
[GOAL]
case t.intro
R : Type u_1
M : Type u_2
P : Type u_3
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
I : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint (↑(partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → ↑(partialSups f) n = ↑(partialSups f) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
[PROOFSTEP]
exact ⟨n, fun m p => (h m).eq_bot_of_ge <| sup_eq_left.1 <| (w (m + 1) <| le_add_right p).symm.trans <| w m p⟩
[GOAL]
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
⊢ N ≃ₗ[R] PUnit
[PROOFSTEP]
apply Nonempty.some
[GOAL]
case h
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
⊢ Nonempty (N ≃ₗ[R] PUnit)
[PROOFSTEP]
obtain ⟨n, w⟩ := IsNoetherian.disjoint_partialSups_eventually_bot (f.tailing i) (f.tailings_disjoint_tailing i)
[GOAL]
case h.intro
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
w : ∀ (m : ℕ), n ≤ m → LinearMap.tailing f i m = ⊥
⊢ Nonempty (N ≃ₗ[R] PUnit)
[PROOFSTEP]
specialize w n (le_refl n)
[GOAL]
case h.intro
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
w : LinearMap.tailing f i n = ⊥
⊢ Nonempty (N ≃ₗ[R] PUnit)
[PROOFSTEP]
apply Nonempty.intro
[GOAL]
case h.intro.val
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
w : LinearMap.tailing f i n = ⊥
⊢ N ≃ₗ[R] PUnit
[PROOFSTEP]
refine (LinearMap.tailingLinearEquiv f i n).symm ≪≫ₗ ?_
[GOAL]
case h.intro.val
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
w : LinearMap.tailing f i n = ⊥
⊢ { x // x ∈ LinearMap.tailing f i n } ≃ₗ[R] PUnit
[PROOFSTEP]
rw [w]
[GOAL]
case h.intro.val
R : Type u_1
M : Type u_2
P : Type u_3
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✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
w : LinearMap.tailing f i n = ⊥
⊢ { x // x ∈ ⊥ } ≃ₗ[R] PUnit
[PROOFSTEP]
apply Submodule.botEquivPUnit
[GOAL]
R : Type ?u.290620
M : Type ?u.290623
inst✝³ : Finite M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ span R ↑(Finite.toFinset (_ : Set.Finite ↑s)) = s
[PROOFSTEP]
rw [Set.Finite.coe_toFinset, Submodule.span_eq]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : IsNoetherian R M
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded] at h ⊢
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded (Submodule.MapSubtype.orderEmbedding N).dual h
[GOAL]
R : Type ?u.294062
inst✝² : Ring R
M : Type ?u.294068
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : IsNoetherian R M
⊢ IsNoetherian R (M ⧸ N)
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded] at h ⊢
[GOAL]
R : Type ?u.294062
inst✝² : Ring R
M : Type ?u.294068
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded (Submodule.comapMkQOrderEmbedding N).dual h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : SMul R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : IsNoetherian R M
⊢ IsNoetherian S M
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded] at h ⊢
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : SMul R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
refine' (Submodule.restrictScalarsEmbedding R S M).dual.wellFounded h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : FG N
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
let ⟨s, hs⟩ := hN
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
haveI := Classical.decEq M
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this : DecidableEq M
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
haveI := Classical.decEq R
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : FG N
s : Finset M
hs : span R ↑s = N
this✝ : DecidableEq M
this : DecidableEq R
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
have : ∀ x ∈ s, x ∈ N := fun x hx => hs ▸ Submodule.subset_span hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
⊢ IsNoetherian R { x // x ∈ N }
[PROOFSTEP]
refine @isNoetherian_of_surjective R ((↑s : Set M) → R) N _ _ _ (Pi.module _ _ _) _ ?_ ?_ isNoetherian_pi
[GOAL]
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
I : IsNoetherianRing 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 }
[PROOFSTEP]
fapply LinearMap.mk
[GOAL]
case refine_1.toAddHom
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
⊢ AddHom (↑↑s → R) { x // x ∈ N }
[PROOFSTEP]
fapply AddHom.mk
[GOAL]
case refine_1.toAddHom.toFun
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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) → { x // x ∈ N }
[PROOFSTEP]
exact fun f => ⟨∑ i in s.attach, f i • i.1, N.sum_mem fun c _ => N.smul_mem _ <| this _ c.2⟩
[GOAL]
case refine_1.toAddHom.map_add'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
⊢ ∀ (x y : ↑↑s → R),
    { val := ∑ i in Finset.attach s, (x + y) i • ↑i, property := (_ : ∑ i in Finset.attach s, (x + y) i • ↑i ∈ N) } =
      { val := ∑ i in Finset.attach s, x i • ↑i, property := (_ : ∑ i in Finset.attach s, x i • ↑i ∈ N) } +
        { val := ∑ i in Finset.attach s, y i • ↑i, property := (_ : ∑ i in Finset.attach s, y i • ↑i ∈ N) }
[PROOFSTEP]
intro f g
[GOAL]
case refine_1.toAddHom.map_add'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
f g : ↑↑s → R
⊢ { val := ∑ i in Finset.attach s, (f + g) i • ↑i, property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
    { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
      { val := ∑ i in Finset.attach s, g i • ↑i, property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case refine_1.toAddHom.map_add'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
f g : ↑↑s → R
⊢ ↑{ val := ∑ i in Finset.attach s, (f + g) i • ↑i, property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
    ↑({ val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
        { val := ∑ i in Finset.attach s, g i • ↑i, property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) })
[PROOFSTEP]
change (∑ i in s.attach, (f i + g i) • _) = _
[GOAL]
case refine_1.toAddHom.map_add'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
f g : ↑↑s → R
⊢ ∑ i in Finset.attach s, (f i + g i) • ↑i =
    ↑({ val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
        { val := ∑ i in Finset.attach s, g i • ↑i, property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) })
[PROOFSTEP]
simp only [add_smul, Finset.sum_add_distrib]
[GOAL]
case refine_1.toAddHom.map_add'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
f g : ↑↑s → R
⊢ ∑ x in Finset.attach s, f x • ↑x + ∑ x in Finset.attach s, g x • ↑x =
    ↑({ val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
        { val := ∑ i in Finset.attach s, g i • ↑i, property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) })
[PROOFSTEP]
rfl
[GOAL]
case refine_1.map_smul'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
⊢ ∀ (r : R) (x : ↑↑s → R),
    AddHom.toFun
        {
          toFun := fun f =>
            { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
          map_add' :=
            (_ :
              ∀ (f g : ↑↑s → R),
                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                    { val := ∑ i in Finset.attach s, g i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun := fun f =>
              { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
            map_add' :=
              (_ :
                ∀ (f g : ↑↑s → R),
                  { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                    { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                      { val := ∑ i in Finset.attach s, g i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
          x
[PROOFSTEP]
intro c f
[GOAL]
case refine_1.map_smul'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
c : R
f : ↑↑s → R
⊢ AddHom.toFun
      {
        toFun := fun f =>
          { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
        map_add' :=
          (_ :
            ∀ (f g : ↑↑s → R),
              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                  { val := ∑ i in Finset.attach s, g i • ↑i, property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        {
          toFun := fun f =>
            { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
          map_add' :=
            (_ :
              ∀ (f g : ↑↑s → R),
                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                    { val := ∑ i in Finset.attach s, g i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
        f
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case refine_1.map_smul'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
c : R
f : ↑↑s → R
⊢ ↑(AddHom.toFun
        {
          toFun := fun f =>
            { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
          map_add' :=
            (_ :
              ∀ (f g : ↑↑s → R),
                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                    { val := ∑ i in Finset.attach s, g i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
        (c • f)) =
    ↑(↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f =>
              { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
            map_add' :=
              (_ :
                ∀ (f g : ↑↑s → R),
                  { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                    { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                      { val := ∑ i in Finset.attach s, g i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
          f)
[PROOFSTEP]
change (∑ i in s.attach, (c • f i) • _) = _
[GOAL]
case refine_1.map_smul'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
c : R
f : ↑↑s → R
⊢ ∑ i in Finset.attach s, (c • f i) • ↑i =
    ↑(↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun f =>
              { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
            map_add' :=
              (_ :
                ∀ (f g : ↑↑s → R),
                  { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                    { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                      { val := ∑ i in Finset.attach s, g i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
          f)
[PROOFSTEP]
simp only [smul_eq_mul, mul_smul]
[GOAL]
case refine_1.map_smul'.a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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
c : R
f : ↑↑s → R
⊢ ∑ x in Finset.attach s, c • f x • ↑x =
    ↑(↑(RingHom.id R) c •
        { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) })
[PROOFSTEP]
exact Finset.smul_sum.symm
[GOAL]
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
I : IsNoetherianRing 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
⊢ LinearMap.range
      {
        toAddHom :=
          {
            toFun := fun f =>
              { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
            map_add' :=
              (_ :
                ∀ (f g : ↑↑s → R),
                  { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                    { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                      { val := ∑ i in Finset.attach s, g i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
        map_smul' :=
          (_ :
            ∀ (c : R) (f : ↑↑s → R),
              AddHom.toFun
                  {
                    toFun := fun f =>
                      { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                    map_add' :=
                      (_ :
                        ∀ (f g : ↑↑s → R),
                          { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                              { val := ∑ i in Finset.attach s, g i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                  (c • f) =
                ↑(RingHom.id R) c •
                  AddHom.toFun
                    {
                      toFun := fun f =>
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                      map_add' :=
                        (_ :
                          ∀ (f g : ↑↑s → R),
                            { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                              { val := ∑ i in Finset.attach s, f i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                { val := ∑ i in Finset.attach s, g i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                    f) } =
    ⊤
[PROOFSTEP]
rw [LinearMap.range_eq_top]
[GOAL]
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
I : IsNoetherianRing 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
    ↑{
        toAddHom :=
          {
            toFun := fun f =>
              { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
            map_add' :=
              (_ :
                ∀ (f g : ↑↑s → R),
                  { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                      property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                    { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                      { val := ∑ i in Finset.attach s, g i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
        map_smul' :=
          (_ :
            ∀ (c : R) (f : ↑↑s → R),
              AddHom.toFun
                  {
                    toFun := fun f =>
                      { val := ∑ i in Finset.attach s, f i • ↑i,
                        property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                    map_add' :=
                      (_ :
                        ∀ (f g : ↑↑s → R),
                          { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                              { val := ∑ i in Finset.attach s, g i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                  (c • f) =
                ↑(RingHom.id R) c •
                  AddHom.toFun
                    {
                      toFun := fun f =>
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                      map_add' :=
                        (_ :
                          ∀ (f g : ↑↑s → R),
                            { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                              { val := ∑ i in Finset.attach s, f i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                { val := ∑ i in Finset.attach s, g i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                    f) }
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case refine_2.mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
⊢ ∃ a,
    ↑{
            toAddHom :=
              {
                toFun := fun f =>
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                map_add' :=
                  (_ :
                    ∀ (f g : ↑↑s → R),
                      { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                          { val := ∑ i in Finset.attach s, g i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : ↑↑s → R),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                        map_add' :=
                          (_ :
                            ∀ (f g : ↑↑s → R),
                              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                { val := ∑ i in Finset.attach s, f i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                  { val := ∑ i in Finset.attach s, g i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                          map_add' :=
                            (_ :
                              ∀ (f g : ↑↑s → R),
                                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                  { val := ∑ i in Finset.attach s, f i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                    { val := ∑ i in Finset.attach s, g i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                        f) }
        a =
      { val := n, property := hn }
[PROOFSTEP]
change n ∈ N at hn
[GOAL]
case refine_2.mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
⊢ ∃ a,
    ↑{
            toAddHom :=
              {
                toFun := fun f =>
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                map_add' :=
                  (_ :
                    ∀ (f g : ↑↑s → R),
                      { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                          { val := ∑ i in Finset.attach s, g i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : ↑↑s → R),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                        map_add' :=
                          (_ :
                            ∀ (f g : ↑↑s → R),
                              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                { val := ∑ i in Finset.attach s, f i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                  { val := ∑ i in Finset.attach s, g i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                          map_add' :=
                            (_ :
                              ∀ (f g : ↑↑s → R),
                                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                  { val := ∑ i in Finset.attach s, f i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                    { val := ∑ i in Finset.attach s, g i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                        f) }
        a =
      { val := n, property := hn }
[PROOFSTEP]
rw [← hs, ← Set.image_id (s : Set M), Finsupp.mem_span_image_iff_total] at hn
[GOAL]
case refine_2.mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn✝ : n ∈ N
hn : ∃ l, l ∈ Finsupp.supported R R ↑s ∧ ↑(Finsupp.total M M R id) l = n
⊢ ∃ a,
    ↑{
            toAddHom :=
              {
                toFun := fun f =>
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                map_add' :=
                  (_ :
                    ∀ (f g : ↑↑s → R),
                      { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                          { val := ∑ i in Finset.attach s, g i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : ↑↑s → R),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                        map_add' :=
                          (_ :
                            ∀ (f g : ↑↑s → R),
                              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                { val := ∑ i in Finset.attach s, f i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                  { val := ∑ i in Finset.attach s, g i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                          map_add' :=
                            (_ :
                              ∀ (f g : ↑↑s → R),
                                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                  { val := ∑ i in Finset.attach s, f i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                    { val := ∑ i in Finset.attach s, g i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                        f) }
        a =
      { val := n, property := hn✝ }
[PROOFSTEP]
rcases hn with ⟨l, hl1, hl2⟩
[GOAL]
case refine_2.mk.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
l : M →₀ R
hl1 : l ∈ Finsupp.supported R R ↑s
hl2 : ↑(Finsupp.total M M R id) l = n
⊢ ∃ a,
    ↑{
            toAddHom :=
              {
                toFun := fun f =>
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                map_add' :=
                  (_ :
                    ∀ (f g : ↑↑s → R),
                      { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                          { val := ∑ i in Finset.attach s, g i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : ↑↑s → R),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                        map_add' :=
                          (_ :
                            ∀ (f g : ↑↑s → R),
                              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                { val := ∑ i in Finset.attach s, f i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                  { val := ∑ i in Finset.attach s, g i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                          map_add' :=
                            (_ :
                              ∀ (f g : ↑↑s → R),
                                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                  { val := ∑ i in Finset.attach s, f i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                    { val := ∑ i in Finset.attach s, g i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                        f) }
        a =
      { val := n, property := hn }
[PROOFSTEP]
refine' ⟨fun x => l x, Subtype.ext _⟩
[GOAL]
case refine_2.mk.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
l : M →₀ R
hl1 : l ∈ Finsupp.supported R R ↑s
hl2 : ↑(Finsupp.total M M R id) l = n
⊢ ↑(↑{
            toAddHom :=
              {
                toFun := fun f =>
                  { val := ∑ i in Finset.attach s, f i • ↑i, property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                map_add' :=
                  (_ :
                    ∀ (f g : ↑↑s → R),
                      { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                          property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                        { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                          { val := ∑ i in Finset.attach s, g i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : ↑↑s → R),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { val := ∑ i in Finset.attach s, f i • ↑i,
                            property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                        map_add' :=
                          (_ :
                            ∀ (f g : ↑↑s → R),
                              { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                  property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                { val := ∑ i in Finset.attach s, f i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                  { val := ∑ i in Finset.attach s, g i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { val := ∑ i in Finset.attach s, f i • ↑i,
                              property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) },
                          map_add' :=
                            (_ :
                              ∀ (f g : ↑↑s → R),
                                { val := ∑ i in Finset.attach s, (f + g) i • ↑i,
                                    property := (_ : ∑ i in Finset.attach s, (f + g) i • ↑i ∈ N) } =
                                  { val := ∑ i in Finset.attach s, f i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, f i • ↑i ∈ N) } +
                                    { val := ∑ i in Finset.attach s, g i • ↑i,
                                      property := (_ : ∑ i in Finset.attach s, g i • ↑i ∈ N) }) }
                        f) }
        fun x => ↑l ↑x) =
    ↑{ val := n, property := hn }
[PROOFSTEP]
change (∑ i in s.attach, l i • (i : M)) = n
[GOAL]
case refine_2.mk.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
l : M →₀ R
hl1 : l ∈ Finsupp.supported R R ↑s
hl2 : ↑(Finsupp.total M M R id) l = n
⊢ ∑ i in Finset.attach s, ↑l ↑i • ↑i = n
[PROOFSTEP]
rw [@Finset.sum_attach M M s _ fun i => l i • i, ← hl2, Finsupp.total_apply, Finsupp.sum, eq_comm]
[GOAL]
case refine_2.mk.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
l : M →₀ R
hl1 : l ∈ Finsupp.supported R R ↑s
hl2 : ↑(Finsupp.total M M R id) l = n
⊢ ∑ a in l.support, ↑l a • id a = ∑ x in s, ↑l x • x
[PROOFSTEP]
refine' Finset.sum_subset hl1 fun x _ hx => _
[GOAL]
case refine_2.mk.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing 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 : M
hn : n ∈ N
l : M →₀ R
hl1 : l ∈ Finsupp.supported R R ↑s
hl2 : ↑(Finsupp.total M M R id) l = n
x : M
x✝ : x ∈ s
hx : ¬x ∈ l.support
⊢ ↑l x • id x = 0
[PROOFSTEP]
rw [Finsupp.not_mem_support_iff.1 hx, zero_smul]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
f : R →+* S
hf : Surjective ↑f
H : IsNoetherianRing R
⊢ IsNoetherianRing S
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_wellFounded] at H ⊢
[GOAL]
R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
f : R →+* S
hf : Surjective ↑f
H : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded (Ideal.orderEmbeddingOfSurjective f hf).dual H
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNilpotent (nilradical R)
[PROOFSTEP]
obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
hn : Ideal.radical ⊥ ^ n ≤ ⊥
⊢ IsNilpotent (nilradical R)
[PROOFSTEP]
exact ⟨n, eq_bot_iff.mpr hn⟩