mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_1.inl
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
exact h.le

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_1.inr
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 = (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
exact h.le

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_2.inr.inl
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h✝ : Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 < (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
exact h.le

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_2.inr.inr
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h✝ : Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 = (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
exact h.le

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
⊢ False

Tactic:
apply hynI

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
⊢ y ∈ I
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_1
α : 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 ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ x ∈ Q

Tactic:
obtain ⟨x', hx', hyx'⟩ := hq hy

Goal state after:
case refine_1
α : 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 ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
x' : α
hx' : x' ∈ P
hyx' : y ≤ x'
⊢ x ∈ Q
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

Tactic:
by
  rw [isSaddlePointOn_iff ha hb]
  refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩
  · exact le_trans (le_of_eq h) (le_of_eq h'.symm)
  · apply le_antisymm
    · exact le_trans h (iInf₂_le a ha)
    · apply le_iSup₂ b hb
  · apply le_antisymm
    · apply iInf₂_le a ha
    · apply le_trans (le_iSup₂ b hb) h

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
h : p ⊓ q ∉ {⊥}
⊢ ∃ y ∈ Q, p ⊓ q ≤ y

Tactic:
grind [inf_le_right]

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P Q : Partition u
⊢ P.Rel ≤ Q.Rel ↔ P ≤ Q

Tactic:
by
  refine ⟨fun h S hS ↦ ?_, fun h a b ⟨t, ht, ha, hb⟩ ↦ ?_⟩
  · obtain ⟨x, hxS⟩ := nonempty_of_mem hS
    obtain ⟨T, hT, hxT, -⟩ := h x x ⟨S, hS, hxS, hxS⟩
    refine ⟨T, hT, fun a haS ↦ ?_⟩
    obtain ⟨T', hT', haT', hxT'⟩ := h a x ⟨S, hS, haS, hxS⟩
    exact eq_of_mem_of_mem hT hT' hxT hxT' ▸ haT'
  obtain ⟨t', ht', htt'⟩ := h ht
  use t', ht', htt' ha, htt' hb

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ P.Rel x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf x = P.partOf y

Tactic:
grind [rel_iff_partOf_eq_partOf_of_mem, Rel.left_mem, Rel.right_mem]

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
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᵐ[μ] 0

Tactic:
by
  rw [predictablePart, ← Finset.sum_const_zero (s := Finset.range n)]
  refine eventuallyEq_sum fun i hi => ?_
  calc
  _ =ᵐ[μ] μ[f (i + 1) | ℱ i] - μ[f i | ℱ i] := by
    simp [condExp_sub (hf.integrable (i + 1)) (hf.integrable i) (ℱ i)]
  _ =ᵐ[μ] f i - f i := (hf.condExp_ae_eq (Nat.le_succ i)).sub (hf.condExp_ae_eq le_rfl)
  _ =ᵐ[μ] 0 := by simp

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

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)

Tactic:
obtain hji | hij := le_total j i

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hji : j ≤ i
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)

case refine_2.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hij : i ≤ j
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case pos
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : n + 1 ≤ m
this : MeasurableSpace Ω := ↑𝓕 n
⊢ MeasurableSet (Function.curry (X m) (n + 1) ⁻¹' {s})

Tactic:
exact ((h n).approx m).measurableSet_fiber s

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✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ μ[f i | ↑𝒢 i] =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]

Tactic:
eventuallyEq_comm,

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✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ μ[f (i + 1) | ↑𝒢 i] =ᵐ[μ] μ[f i | ↑𝒢 i]
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, upcrossings a b f ω < ∞

Tactic:
refine ae_lt_top (hf.stronglyAdapted.measurable_upcrossings hab) ?_

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ∃ j, m ≤ j ∧ u j ω ∈ s
t : ι
ht : m ≤ t ∧ u t ω ∈ s
⊢ ⊤ ≤ ↑(sInf {j | m ≤ j ∧ u j ω ∈ s})

Tactic:
exact absurd ⟨t, hnm.trans ht.1, ht.2⟩ h_n

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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun j ↦ f (j + 1) ω - f j ω) x

Tactic:
have 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 ω : ℕ)) ω := by
    intro k
    rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]
    · rfl
    · ext i
      simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
      exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le

Goal state after:
case neg
Ω : 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 ω)) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun j ↦ f (j + 1) ω - f j ω) x
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
intro i ω

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

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ MeasurableSpace Ω

pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ ?refine_1 ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
· exact f ⊥

Goal state after:
case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ ↑f ⊥ ≤ hτ.measurableSpace

case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ MeasurableSpace Ω

pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ ?refine_1 ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
· exact f ⊥

Goal state after:
case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ ↑f ⊥ ≤ hτ.measurableSpace

case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
⊢ i < a ∨ i = a ↔ a = i ∨ i < a

Tactic:
rw [@eq_comm _ i, or_comm]

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
⊢ i < a ∨ i = a ↔ a = i ∨ i < a

Tactic:
rw [@eq_comm _ i, or_comm]

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
⊢ μ[f | m₂] =ᵐ[μ] fun x ↦ ∫ (x : Ω), f x ∂μ

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint
    (fun s _ hs ↦ integrableOn_const hs.ne) (fun s hms hs => ?_)
      stronglyMeasurable_const.aestronglyMeasurable).symm

Goal state after:
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ = ∫ (x : Ω) in s, f x ∂μ
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:

Tactic:
_ ≤ ENNReal.ofReal
          (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) +
        ENNReal.ofReal
          (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      gcongr with ω hω
      · exact smul_le_stoppedValue_hittingBtwn hsub n
      · exact (hsub.integrable n).integrableOn
      · refine Integrable.integrableOn ?_
        refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)
        exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici
      · exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const
      rw [Set.mem_ofPred_eq] at hω
      have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_ofPred_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
      simp only [stoppedValue, this, ge_iff_le]
      refine le_of_eq ?_
      congr
    _ = ENNReal.ofReal
        (∫ ω, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ (μ := μ)]
        convert! rfl
        ext ω
        change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => hnonneg _ _]
    _ ≤ ENNReal.ofReal (μ[f n]) := by
      refine ENNReal.ofReal_le_ofReal ?_
      rw [← stoppedValue_const f n]
      refine hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)
      simp [hittingBtwn_le]

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ

Tactic:
rwa [← integral_congr_ae huv, ←
      (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mpr
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n ↦ f n ω)
⊢ False

Tactic:
exact hω₂ ((tendsto_atBot_add_left_of_ge _ b fun n =>
      hbdd ⟨n, rfl⟩) <| tendsto_neg_atBot_iff.2 ht)

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

Goal state before:
pp: case e_μ
E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ ∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν =
    ∫ (x : ℝ), x ∂gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal)

Tactic:
simp [variance_nonneg]

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

Goal state before:
pp: case e_v
E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal =
    Var[id; gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal)].toNNReal

Tactic:
simp [variance_nonneg]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : ¬MemLp id 2 μ
⊢ covarianceOperator μ = 0

Tactic:
by
  ext x
  refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm
  simp [hμ, uncenteredCovarianceBilinDual_of_not_memLp]

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

Goal state before:
pp: case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ⋯
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ Integrable (fun x ↦ ‖c‖ ^ p.toReal) μ

Tactic:
have I : Integrable (fun (x : E) ↦ ‖x‖) μ := by
    apply Integrable.norm
    contrapose hx
    exact integral_undef hx

Goal state after:
case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
I : Integrable (fun x ↦ ‖x‖) μ
⊢ Integrable (fun x ↦ ‖c‖ ^ p.toReal) μ