-- Mathlib/Probability/Martingale/Centering.lean
theorem predictablePart_add_ae_eq [SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E}
    (hf : Martingale f ℱ μ) (hg : Adapted ℱ fun n => g (n + 1)) (hg0 : g 0 = 0)
    (hgint : ∀ n, Integrable (g n) μ) (n : ℕ) : predictablePart (f + g) ℱ μ n =ᵐ[μ] g n

Proof state:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω

Tactic:
rw [Pi.add_apply, Pi.add_apply, hω]

Result:
no goals

Proof state:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ predictablePart (f + g) ℱ μ n ω = g n ω

Tactic:
rw [← add_right_inj (f n ω)]

Result:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω

Proof state:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω

Tactic:
conv_rhs => rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]

Result:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ predictablePart (f + g) ℱ μ n =ᶠ[ae μ] g n

Tactic:
filter_upwards [martingalePart_add_ae_eq hf hg hg0 hgint n] with ω hω

Result:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : Adapted ℱ fun n => g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ predictablePart (f + g) ℱ μ n ω = g n ω