-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem iSup_succ_eq_sup {α} (f : ℕ → α → ℝ≥0∞) (m : ℕ) (a : α) :
    ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a = f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a

Proof state:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ∧
    f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Tactic:
constructor

Result:
case left
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

case right
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Proof state:
case left.inr
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
h : n = m.succ
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
exact h ▸ le_sup_left

Result:
no goals

Proof state:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ c = d

Tactic:
rw [le_antisymm_iff, hc, hd]

Result:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ∧
    f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Proof state:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
⊢ c = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
set d := f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a with hd

Result:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ c = d

Proof state:
case left
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
rcases Nat.of_le_succ hn with (h | h)

Result:
case left.inl
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
h : n ≤ m
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

case left.inr
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
h : n = m.succ
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Proof state:
case left.inl
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
h : n ≤ m
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
exact le_sup_of_le_right (le_iSup₂ (f := fun k (_ : k ≤ m) ↦ f k a) n h)

Result:
no goals

Proof state:
case right
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Tactic:
refine sup_le ?_ (biSup_mono fun n hn ↦ hn.trans m.le_succ)

Result:
case right
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ f m.succ a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Proof state:
case left
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
refine iSup₂_le fun n hn ↦ ?_

Result:
case left
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
n : ℕ
hn : n ≤ m + 1
⊢ f n a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Proof state:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Tactic:
set c := ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a with hc

Result:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
⊢ c = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a

Proof state:
case right
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
⊢ f m.succ a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Tactic:
exact @le_iSup₂ ℝ≥0∞ ℕ (fun i ↦ i ≤ m + 1) _ _ (m + 1) le_rfl

Result:
no goals