Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : β → Type u_7} [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)]
        [∀ (i : β), IsNoetherian R (M i)], IsNoetherian R ((i : β) → M i)

pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Type u_7} [inst : (i : PEmpty.{u_6 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_6 + 1}) → Module R (M i)] [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R (M i)],
    IsNoetherian R ((i : PEmpty.{u_6 + 1}) → M i)

pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : Option α → Type u_7} [inst : (i : Option α) → AddCommGroup (M i)]
        [inst_1 : (i : Option α) → Module R (M i)] [∀ (i : Option α), IsNoetherian R (M i)],
        IsNoetherian R ((i : Option α) → M i)

Tactic:
· exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Type u_7} [inst : (i : PEmpty.{u_6 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_6 + 1}) → Module R (M i)] [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R (M i)],
    IsNoetherian R ((i : PEmpty.{u_6 + 1}) → M i)

R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : Option α → Type u_7} [inst : (i : Option α) → AddCommGroup (M i)]
        [inst_1 : (i : Option α) → Module R (M i)] [∀ (i : Option α), IsNoetherian R (M i)],
        IsNoetherian R ((i : Option α) → M i)