mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
⊢ ∀ {w x y z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)

Tactic:
intro w _ _ _ h1 h2
    have compatible_left_sup {x y t : α} (hh : r x y) : r (x ⊔ t) (y ⊔ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊔ t) _ _ ((x ⊔ y) ⊔ t)
        (sup_le_sup_right inf_le_left _) (sup_le_sup_right le_sup_left _)
        (sup_le_sup_right inf_le_right _) (sup_le_sup_right le_sup_right _)
        (h₄ inf_le_sup (h₂.mp hh)).2
    exact transitive h₂ h₃ h₄ (by
      simpa [sup_comm w] using compatible_left_sup h2)
      (compatible_left_sup h1)

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite ↑((fun a ↦ π ⋯ a.snd) ⁻¹' {a₀})
⊢ (fun a ↦ π ⋯ a.snd) ⁻¹' {a₀} ⊆ Ici ⟨0, a₀⟩

Tactic:
simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite ↑((fun a ↦ π ⋯ a.snd) ⁻¹' {a₀})
⊢ ∀ (a : ℕ) (b : α a), π ⋯ b = a₀ → ⟨0, a₀⟩ ≤ ⟨a, b⟩
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2
α : Type u_1
s t x✝ y✝ z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
x' : α
hx' : x' ∈ Q
hyx' : y ≤ x'
⊢ x ∈ P

Tactic:
obtain rfl := Q.pairwiseDisjoint.eq_of_le h hx' (Q.ne_bot_of_mem h) (hxy.trans hyx')

Goal state after:
case refine_2
α : Type u_1
s t x✝ y✝ z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
hx' : x ∈ Q
hyx' : y ≤ x
⊢ x ∈ P
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ x ∈ S

Tactic:
by
    rw [le_antisymm le_restrictAux hx]
    exact S.sInf_mem <| by simp +contextual [Set.subset_def]

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ predictablePart f ℱ μ 0 = 0

Tactic:
simp_rw [predictablePart, Finset.range_zero, Finset.sum_empty]

Goal state after:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
⊢ Submartingale (fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

Tactic:
have hint : ∀ m, Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ := fun m =>
      integrable_finsetSum' _ fun i _ => Integrable.bdd_smul
        ((hf.integrable _).sub (hf.integrable _)) (C i)
        hξ.stronglyMeasurable.aestronglyMeasurable (ae_of_all _ (hC i))

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
⊢ Submartingale (fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
⊢ MeasurableSet {ω | τ ω ≤ ↑i}

Tactic:
have h_eq_iUnion : {ω | τ ω ≤ i} = ⋃ k ≤ i, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_ofPred_eq, Set.mem_iUnion, exists_prop]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
h_eq_iUnion : {ω | τ ω ≤ ↑i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k}
⊢ MeasurableSet {ω | τ ω ≤ ↑i}
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

pp: case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
· rw [isBoundedUnder_le_abs] at h
    refine tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2
    rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ hab
    exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne

Goal state after:
case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
⊢ 0 ≤
    f (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω)).untopA ω -
      f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω

Tactic:
upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
⊢ 0 ≤ f (↑N).untopA ω - f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑c ∧ ↑c < π ω}.indicator (f (c + 1) - f c) a ∂μ

Tactic:
rw [integral_finsetSum]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
⊢ 0 ≤ ∑ i ∈ Finset.range (N + 1), ∫ (a : Ω), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (f (i + 1) - f i) a ∂μ

case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
⊢ ∀ i ∈ Finset.range (N + 1), Integrable ({ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (f (i + 1) - f i)) μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
ω : Ω
i : ℕ
⊢ f i ω - a ≤ 0 ↔ f i ω ≤ a

Tactic:
sub_nonpos

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
ω : Ω
i : ℕ
⊢ f i ω ≤ a ↔ f i ω ≤ a
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ ↑(min (↑i) (σ ω)).untopA ≤ τ ω

Tactic:
· refine le_trans ?_ hστ
      simp [untopA_eq_untop]

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
integral_sub h_int (integrable_const _)

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ u (τ y).untopA y = ∑ c ∈ s, {ω | τ ω = ↑c}.indicator (u c) y

Tactic:
Finset.sum_indicator_eq_sum_filter

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ u (τ y).untopA y = ∑ i ∈ s with y ∈ {ω | τ ω = ↑i}, u i y
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ u n ω = u n ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

pp: case inl.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ω ∈ {a | ↑n ≤ τ a}

Tactic:
Finset.sum_eq_zero,

Goal state after:
case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ u n ω = u n ω + 0

case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ∀ x ∈ {i ∈ s | i < n}, {ω | τ ω = ↑x}.indicator (u x) ω = 0

case inl.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ω ∈ {a | ↑n ≤ τ a}
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |(s (n + 1)).indicator 1 ω| ≤ 1

Tactic:
← Real.norm_eq_abs,

Goal state after:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ ‖(s (n + 1)).indicator 1 ω‖ ≤ 1
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
⊢ stoppedProcess u τ n = {a | ↑n ≤ τ a}.indicator (u n) + ∑ i < n, {ω | τ ω = ↑i}.indicator (u i)

Tactic:
have h_mem : ∀ ω, τ ω < n → τ ω ∈ WithTop.some '' (Finset.Iio n) := by
    intro ω h
    simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]
    have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
    lift τ ω to ι using h_top with i hi
    exact ⟨i, mod_cast h, rfl⟩
  rw [stoppedProcess_eq_of_mem_finset n h_mem]
  congr with i
  simp

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
⊢ Integrable (stoppedValue u τ) μ

Tactic:
refine integrable_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic N)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp (↑z.re * ↑(X ω)) * cexp (↑z.im * I * ↑(X ω)) ∂μ‖ ≤ mgf X μ (↑z.re + ↑z.im * I).re

Tactic:
re_add_im

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp (↑z.re * ↑(X ω)) * cexp (↑z.im * I * ↑(X ω)) ∂μ‖ ≤ mgf X μ z.re
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

Tactic:
← RCLike.re_eq_complex_re,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ RCLike.re (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ) = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)) ℙ

Tactic:
refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹

Goal state after:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ 0 < ↑(2 * v)⁻¹
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
by
  rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
  exact hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω ↦ ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
hasDerivAt_iff_hasFDerivAt

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h :
  HasFDerivAt (complexMGF X μ)
    (ContinuousLinearMap.toSpanSingleton ℂ (∫ (x : Ω), (fun ω ↦ ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ)) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
by
  induction n generalizing z with
  | zero => simp [hasDerivAt_complexMGF hz]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ MemLp X (↑p) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet h

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
⊢ MemLp X (↑p) μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ Integrable (fun x ↦ rexp (t * x)) (gaussianReal μ v)

Tactic:
rw [← mgf_pos_iff, mgf_gaussianReal (μ := μ) (v := v) (by simp)]

Goal state after:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ 0 < rexp (μ * t + ↑v * t ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)

Tactic:
rw [← Real.exp_add]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hbc
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)

Tactic:
exact sq_normThreshold_add_one_le n

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : InnerProductSpace ℝ E
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (Measure.map (fun ω ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (Measure.map X P) t.ofLp.1 * charFun (Measure.map Y P) t.ofLp.2

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
⊢ (x + y) ⟨t₀ + t, ⋯⟩ - (x + y) ⟨t₀, ⋯⟩ = x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩ + (y ⟨t₀ + t, ⋯⟩ - y ⟨t₀, ⋯⟩)

Tactic:
simp; abel

Goal state after: