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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ sSup (⇑f '' (principal x).left) = f x

Tactic:
apply le_antisymm (by simp)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ f x ≤ sSup (⇑f '' (principal x).left)
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s✝ : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x✝ : Concept α β r
hc : x✝ ∈ s
⊢ x✝ ≤ sSup s

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s✝ : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x✝ : Concept α β r
hc : x✝ ∈ upperBounds s
⊢ sSup s ≤ x✝

Tactic:
· exact intent_subset_intent_iff.1 <| biInter_subset_of_mem hc

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s✝ : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x✝ : Concept α β r
hc : x✝ ∈ upperBounds s
⊢ sSup s ≤ x✝
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mpr.univ
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
⊢ Set.univ ∈ f

Tactic:
exact univ_mem

Goal state after:
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))

Tactic:
by
  rw [← Ioi_union_left, ← Ioi_union_left]
  exact
    (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union
      (@image_singleton _ _ f a ▸ surjOn_image _ _)

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i

Tactic:
obtain ⟨f, h0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite_of_bot hfin
  refine ⟨f, h0, hf, fun i ↦ ?_⟩
  induction i with
  | zero => simp [h0]
  | succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊔ y✝) (x✝² ⊔ z✝)

Tactic:
simp_all +instances only [Setoid.ker, onFun, map_sup]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x : P
⊢ x ∈ ↑J

Tactic:
rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : y ∉ ↑I
⊢ x ∈ ↑J
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_1.a
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
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
simp only [iSup_le_iff]

Goal state after:
case refine_1.a
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
h : IsSaddlePointOn X Y f a b
⊢ ∀ i ∈ Y, f a i ≤ f a b
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let ⟨b₁, ⟨b₁J, cba₁⟩⟩ := (Lattice.mem_ideal_sup_principal a₁ c₁ J).1 c₁J₁

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ ∃ t ∈ P, x ∈ t

Tactic:
rwa [← P.sUnion_eq, mem_sUnion] at hx

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

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
MeasurableSpace.map_def

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2.hs
Ω : 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 (ℕ × Ω) := ⋯
X : ℕ → ℕ × Ω → E := ⋯
Y : ℕ → ℕ × Ω → E := ⋯
m : ℕ
⊢ (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)).Finite

Tactic:
refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)

Goal state after:
case refine_2.hs
Ω : 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 n : ℕ
hn : n ∈ ↑(Finset.range (m + 1))
⊢ (Set.range (Function.curry (X m) n)).Finite
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
by
  rw [upperCrossingTime]

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

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
        (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
      refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
      rw [Nat.lt_pred_iff] at hm
      convert! Nat.find_min _ hm

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
hmono : StrictMonoOn (fun n ↦ upperCrossingTime a b f N n ω) (Set.Iic (Nat.find ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
    have := exists_seq_forall_of_frequently h_freq
    simp_rw [tendsto_nhdsWithin_iff] at this
    obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
    exact ⟨s, hs_gt, hs_tendsto⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
u : WithTop ι
hu : ↑t < u
⊢ ∃ i, ↑(s i) < u

Tactic:
refine Eventually.exists (f := atTop) ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
u : WithTop ι
hu : ↑t < u
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(s x) < u
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet {ω | ⨅ n ∈ s, τ n ω < ↑i}ᶜ

Tactic:
rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet (⋂ n ∈ s, {ω | ↑i ≤ τ n ω})

Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ {ω | ⨅ n ∈ s, τ n ω < ↑i}ᶜ = ⋂ n ∈ s, {ω | ↑i ≤ τ n ω}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
i : ι
⊢ MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})

Tactic:
replace hs := fun i ↦ (hs i).2

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
⊢ MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by
  have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_ofPred_eq, Set.mem_sdiff]
  rw [this]
  exact (hτ.measurableSet_le' i).diff (hτ.measurableSet_eq_of_countable_range' h_countable i)

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

Goal state before:
pp: case pos
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
⊢ f (min (↑i) (leastGE f r ω)).untopA ω ≤ r + ↑R

Tactic:
simp only [h_zero, hf0, Pi.zero_apply]
    positivity

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_4
Ω : 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 < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

Tactic:
have h_integral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ := by
      simpa using! continuous_integral.comp (ContinuousLinearMap.continuous (Submodule.subtypeL _))

Goal state after:
case pos.refine_4
Ω : 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 < ∞
h_integral : Continuous fun f ↦ ∫ (x : Ω), ↑↑↑f x ∂μ
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf X μ = mgf Y μ'

Tactic:
by
  rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_
  rw [exp_add]
  exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω|)) μ

Tactic:
by
  rcases le_total 0 t with ht_nonneg | ht_nonpos
  · simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs ht_int_pos ht_int_neg
  · simp_rw [abs_of_nonpos ht_nonpos]
    exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ complexMGF X μ (↑t * I) = charFun (Measure.map X μ) t

Tactic:
rw [← complexMGF_id_map hX, complexMGF_id_mul_I]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (mgf X μ) t

Tactic:
← re_complexMGF_ofReal'

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (fun x ↦ (complexMGF X μ ↑x).re) t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)

Tactic:
have : |t| = |t| - x + x := by simp

Goal state after:
case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x ↦ NormedSpace.exp (x • ↑(X ω))) (↑(X ω) • NormedSpace.exp (ε • ↑(X ω))) ε

Tactic:
convert! hasDerivAt_exp_smul_const (X ω : ℂ) ε using 1

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ↑(X ω) • NormedSpace.exp (ε • ↑(X ω)) = NormedSpace.exp (ε • ↑(X ω)) * ↑(X ω)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this✝ : NeZero μ
this : NeZero μ'
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ ↔ Integrable (fun ω ↦ rexp (t * Y ω)) μ'

Tactic:
rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ deriv (fun t ↦ μ * t + ↑v * t ^ 2 / 2) 0 = μ

Tactic:
deriv_fun_add (by fun_prop) (by fun_prop),

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ deriv (HMul.hMul μ) 0 + deriv (fun t ↦ ↑v * t ^ 2 / 2) 0 = μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity),
      ← Real.rpow_mul (by positivity), mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ‖L‖ * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ n, x ≤ t n
h' : ∀ m < Nat.find h, ¬x ≤ t m
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)

Tactic:
simp only [not_le] at h'

Goal state after:
β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ n, x ≤ t n
h' : ∀ m < Nat.find h, t m < x
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∑ i, ∑ j, cov[fun ω ↦ x.ofLp i * X i ω, fun ω ↦ y.ofLp j * X j ω; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]

pp: case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∀ (i : ι), MemLp (fun ω ↦ x.ofLp i * X i ω) 2 μ

pp: case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∀ (i : ι), MemLp (fun ω ↦ y.ofLp i * X i ω) 2 μ

Tactic:
· refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_
      rw [covariance_const_mul_left, covariance_const_mul_right]
      ring

Goal state after:
case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∀ (i : ι), MemLp (fun ω ↦ x.ofLp i * X i ω) 2 μ

case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ ∀ (i : ι), MemLp (fun ω ↦ y.ofLp i * X i ω) 2 μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h : (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) = (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S))
⊢ IsGaussian (multivariateGaussian μ S)

Tactic:
simp only [multivariateGaussian]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h : (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) = (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S))
⊢ IsGaussian (Measure.map (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) (stdGaussian (EuclideanSpace ℝ ι)))