case intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
⊢ ∃ n₀, ∀ (n : ℕ), N F (n + n₀) ≤ N F' n ∧ N F' (n + n₀) ≤ N F n
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
⊢ ∃ n₀, ∀ (n : ℕ), N F (n + n₀) ≤ N F' n ∧ N F' (n + n₀) ≤ N F n
obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
⊢ ∃ n₀, ∀ (n : ℕ), N F (n + n₀) ≤ N F' n ∧ N F' (n + n₀) ≤ N F n
case intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
⊢ ∃ n₀, ∀ (n : ℕ), N F (n + n₀) ≤ N F' n ∧ N F' (n + n₀) ≤ N F n
obtain ⟨n₂, h₂⟩ := h'.exists_forall_le (le_of_eq e.symm)
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
⊢ ∀ (n : ℕ), N F (n + max n₁ n₂) ≤ N F' n ∧ N F' (n + max n₁ n₂) ≤ N F n
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
⊢ ∃ n₀, ∀ (n : ℕ), N F (n + n₀) ≤ N F' n ∧ N F' (n + n₀) ≤ N F n
use max n₁ n₂
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
n : ℕ
⊢ N F (n + max n₁ n₂) ≤ N F' n ∧ N F' (n + max n₁ n₂) ≤ N F n
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
⊢ ∀ (n : ℕ), N F (n + max n₁ n₂) ≤ N F' n ∧ N F' (n + max n₁ n₂) ≤ N F n
intro n
no goals
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h✝ h : Stable F
h' : Stable F'
e : N F 0 = N F' 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), N F (n + n₁) ≤ N F' n
n₂ : ℕ
h₂ : ∀ (n : ℕ), N F' (n + n₂) ≤ N F n
n : ℕ
⊢ N F (n + max n₁ n₂) ≤ N F' n ∧ N F' (n + max n₁ n₂) ≤ N F n
refine' ⟨(F.antitone _).trans (h₁ n), (F'.antitone _).trans (h₂ n)⟩ <;> simp