-- Mathlib/RingTheory/Filtration.lean
theorem Stable.bounded_difference (h : F.Stable) (h' : F'.Stable) (e : F.N 0 = F'.N 0) :
    ∃ n₀, ∀ n, F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
use max n₁ n₂

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
⊢ ∀ (n : ℕ), F.N (n + n₁ ⊔ n₂) ≤ F'.N n ∧ F'.N (n + n₁ ⊔ n₂) ≤ F.N n

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ F.N (n + n₁ ⊔ n₂) ≤ F'.N n ∧ F'.N (n + n₁ ⊔ n₂) ≤ F.N n

Tactic:
refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩ <;> simp

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
⊢ ∀ (n : ℕ), F.N (n + n₁ ⊔ n₂) ≤ F'.N n ∧ F'.N (n + n₁ ⊔ n₂) ≤ F.N n

Tactic:
intro n

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ F.N (n + n₁ ⊔ n₂) ≤ F'.N n ∧ F'.N (n + n₁ ⊔ n₂) ≤ F.N n

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
obtain ⟨n₂, h₂⟩ := h'.exists_forall_le (le_of_eq e.symm)

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n