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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ findAtom ⊥ = ⊥

Tactic:
apply Function.iterate_fixed
  simp

Goal state after:
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:
rw [le_antisymm le_restrictAux hx]
    exact S.sInf_mem <| by simp +contextual [Set.subset_def]

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ (type α).card = #α

Tactic:
by
  rw [card, liftOn_type]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : ↑(Set.singleton (n + 1)) × Ω
⊢ p ∈ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A ↔ p ∈ ∅

Tactic:
simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
          iff_false, not_and]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : ↑(Set.singleton (n + 1)) × Ω
⊢ i < ↑p.1 → p.2 ∉ A
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
⊢ u k ω ∉ s

Tactic:
by
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hittingBtwn, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩

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✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᵐ[μ] μ[f k | ↑𝒢 i]
ω : Ω
hω1 : f i ω ≤ μ[f k | ↑𝒢 i] ω
hω2 : μ[f k | ?m.143] ω ≤ μ[μ[f (k + 1) | ↑𝒢 k] | ?m.143] ω
hω3 : μ[μ[f (k + 1) | ↑𝒢 k] | ↑𝒢 i] ω = μ[f (k + 1) | ↑𝒢 i] ω
⊢ f i ω ≤ μ[f (k + 1) | ↑𝒢 i] ω

Tactic:
hω1,

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✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᵐ[μ] μ[f k | ↑𝒢 i]
ω : Ω
hω1 : f i ω ≤ μ[f k | ↑𝒢 i] ω
hω2 : μ[f k | ?m.143] ω ≤ μ[μ[f (k + 1) | ↑𝒢 k] | ?m.143] ω
hω3 : μ[μ[f (k + 1) | ↑𝒢 k] | ↑𝒢 i] ω = μ[f (k + 1) | ↑𝒢 i] ω
⊢ μ[f k | ↑𝒢 i] ω ≤ μ[f (k + 1) | ↑𝒢 i] ω
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✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
n : ℕ
⊢ f n =ᵐ[μ] f 0

Tactic:
by
  induction n with
  | zero => rfl
  | succ k ih =>
    exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
      (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
⊢ Monotone fun N ω ↦ upcrossingsBefore a b f N ω

Tactic:
intro N M hNM ω

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ (fun N ω ↦ upcrossingsBefore a b f N ω) N ω ≤ (fun N ω ↦ upcrossingsBefore a b f N ω) M ω
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
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
⊢ ↑‖a‖₊ * μ Set.univ < ∞

Tactic:
finiteness

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

Goal state before:
pp: case refine_1
Ω : 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
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
n : ℕ
ω : Ω
⊢ ↑‖f n ω - a‖₊ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case h0
Ω : 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
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0 ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ 0

Tactic:
left

Goal state after:
case h0
Ω : 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
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case ht
Ω : 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
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞ ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ∞

Tactic:
left

Goal state after:
case ht
Ω : 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
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case ht
Ω : 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
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: Ω : 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:
refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Goal state after:
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 Ω

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

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: Ω : 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:
refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Goal state after:
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 Ω

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

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.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m ↦ eLpNorm μ[f m - g | ↑ℱ n] 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
⊢ μ[f m | ↑ℱ n] - μ[g | ↑ℱ n] =ᵐ[μ] f n - μ[g | ↑ℱ n]

Tactic:
filter_upwards [hf.2 n m hm] with x hx

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m ↦ eLpNorm μ[f m - g | ↑ℱ n] 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
x : Ω
hx : μ[f m | ↑ℱ n] x = f n x
⊢ (μ[f m | ↑ℱ n] - μ[g | ↑ℱ n]) x = (f n - μ[g | ↑ℱ n]) x
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ ∀ a ∈ Finset.range n, μ (s (a + 1)) ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  (∀ i ∈ s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ) →
    AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i_1 ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Tactic:
have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec

Goal state after:
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))
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2) ∨ √(2 * π) = 0

Tactic:
left

Goal state after:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := ⋯
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : interior (integrableExpSet X μ) = ∅
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)}

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
h_empty : ¬interior (integrableExpSet X μ) = ∅
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
· simp [h_empty]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : ¬interior (integrableExpSet X μ) = ∅
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)}
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_v
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (L 1 ^ 2).toNNReal * v = (max (L 1 ^ 2) 0).toNNReal * (↑v).toNNReal

Tactic:
Real.toNNReal_coe

Goal state after:
case e_v
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (L 1 ^ 2).toNNReal * v = (max (L 1 ^ 2) 0).toNNReal * v
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2

Tactic:
by
  have hu : UniqueDiffOn ℝ (Set.Icc 0 t) := uniqueDiffOn_Icc ht
  rw [← sub_zero (cgf X μ t)]
  nth_rw 3 [← sub_zero t]
  rw [← Set.uIoo_of_lt ht]
  convert! taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_
  · have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0 := by
      convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
      · simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm
      · exact hu 0 ⟨le_refl 0, le_of_lt ht⟩
    simp [hd, Set.uIcc_of_lt ht]
  · rw [Set.uIcc_of_lt ht]
    exact (analyticOn_cgf.mono hs).contDiffOn hu

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

Goal state before:
pp: case neg
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : ¬MemLp id 2 μ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

Tactic:
simp [h, variance_of_not_memLp, aestronglyMeasurable_id]

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

Goal state before:
pp: case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - ∫ (x : E), c + x ∂μ⟫ * ⟪y, c + z - ∫ (x : E), c + x ∂μ⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

Tactic:
rw [integral_add (integrable_const _)]

Goal state after:
case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ * ⟪y, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ Integrable (fun x ↦ x) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg
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
⊢ MemLp (fun x ↦ c) p μ

Tactic:
rcases eq_or_ne p 0 with rfl | hp0

Goal state after:
case neg.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (fun x ↦ x - c) 0 μ
⊢ MemLp (fun x ↦ c) 0 μ

case neg.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
⊢ MemLp (fun x ↦ c) p μ
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 :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable ((fun y_1 ↦ rexp (C * ‖y + y_1‖ ^ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y + -x‖ ∨ C = 0

Tactic:
left

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 :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable ((fun y_1 ↦ rexp (C * ‖y + y_1‖ ^ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y + -x‖
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 1 - μ {x | ‖x‖ ≤ a} ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case refine_1
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c < ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ c ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d < ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c < ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hd
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - d < ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ c ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c < ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ gaussianReal 0 (↑↑s).toNNReal = gaussianReal 0 ↑s

Tactic:
Real.toNNReal_coe

Goal state after:
I : Finset ℝ≥0
s : ↥I
⊢ gaussianReal 0 ↑s = gaussianReal 0 ↑s
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ (↑(↑s + ↑t - 2 * min ↑s ↑t)).toNNReal = nndist ↑s ↑t

pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t

Tactic:
Real.toNNReal_coe

Goal state after:
case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t

case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s

pp: case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑s

Tactic:
· rw [add_comm, min_comm]

Goal state after:
case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑s
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s ⟂ᵢ[P] X t - X s

Tactic:
by
  refine (hX.indepFun_sub_sub hrs hst).congr ?_ .rfl
  filter_upwards [h] with ω hω using by simp [hω]

Goal state after: