mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x

Tactic:
mul_nat_iff hn

Goal state after:
p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ ⋂ i, upperBounds {u i} = ⋂ i, upperBounds (s i)

Tactic:
upperBounds_singleton,

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ ⋂ i, Ici (u i) = ⋂ i, upperBounds (s i)
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
⊢ Tendsto Subtype.val atTop atTop

Tactic:
have h_mono : Monotone ((↑) : Nat.Primes → ℕ) := fun p q hpq => hpq

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
h_mono : Monotone Subtype.val
⊢ Tendsto Subtype.val atTop atTop
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this✝ : SemilatticeSup Nat.Primes := ⋯
μ : Measure 𝕊 := ⋯
u : Nat.Primes → 𝕊 := ⋯
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := ⋯
X : ℕ → Set 𝕊 := ⋯
A : ℕ → Set 𝕊 := ⋯
B : ℕ → Set 𝕊 := ⋯
C : ℕ → Set 𝕊 := ⋯
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := ⋯
f : 𝕊 → 𝕊 := ⋯
this : f '' B p ⊆ blimsup (fun n ↦ approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
⊢ (blimsup (fun n ↦ approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n) =ᵐ[volume] B p

Tactic:
exact blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∣∣n) (fun n => {y | addOrderOf y = n})
        (Nat.cast_pos.mpr hp.pos) _ hδ

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s t : Set α
ht : ∀ (t' : Set α), s ⊆ t' → CountableSupClosed t' → t ⊆ t'
ht_ne : t.Nonempty
⊢ t.Countable → ∀ (x : α), IsLUB t x → ∀ (t : Set α), s ⊆ t → CountableSupClosed t → x ∈ t

Tactic:
ht_c

Goal state after:
α : Type u_2
inst✝ : Preorder α
s t : Set α
ht : ∀ (t' : Set α), s ⊆ t' → CountableSupClosed t' → t ⊆ t'
ht_ne : t.Nonempty
ht_c : t.Countable
⊢ ∀ (x : α), IsLUB t x → ∀ (t : Set α), s ⊆ t → CountableSupClosed t → x ∈ t
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ x✝ ∩ y✝ ∈ {s | r.core s ∈ l}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ r.core (x✝ ∩ y✝) ∈ l
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I

Tactic:
exact IF.I.isIdeal

Goal state after:
Module: Mathlib.Order.TeichmullerTukey

Goal state before:
pp: α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
⊢ ∃ m, x ⊆ m ∧ Maximal (fun x ↦ x ∈ F) m

Tactic:
refine zorn_subset_nonempty F (fun c cF cch cne ↦
    ⟨sUnion c, ?_, fun s sc ↦ subset_sUnion_of_mem sc⟩) x xF
  /- Prove that the union belongs to `F`. -/
  refine (hF (sUnion c)).mpr fun s sc sfin ↦ ?_
  /- Use the finite character property and the fact that any finite subset of the union is also a
  subset of some element of the chain. -/
  obtain ⟨t, tc, st⟩ := cch.directedOn.exists_mem_subset_of_finite_of_subset_sUnion cne sfin sc
  exact (hF t).mp (cF tc) s st sfin

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

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)
⊢ Nonempty (α ≃o β)

Tactic:
← type_ulift,

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) = lift.{u_1, u} (type β)
⊢ Nonempty (α ≃o β)
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) = lift.{u_1, u} (type β)
⊢ Nonempty (α ≃o β)

Tactic:
← type_ulift,

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) = type (ULift β)
⊢ Nonempty (α ≃o β)
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β)
⊢ Nonempty (α ↪o β)

Tactic:
← type_ulift,

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) ≤ lift.{u_1, u} (type β)
⊢ Nonempty (α ↪o β)
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) ≤ lift.{u_1, u} (type β)
⊢ Nonempty (α ↪o β)

Tactic:
← type_ulift,

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : type (ULift α) ≤ type (ULift β)
⊢ Nonempty (α ↪o β)
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ InfClosed ↑S

Tactic:
by
  rintro a ha b hb; rw [← sInf_pair]; exact S.sInf_mem (pair_subset ha hb)

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m)) (n + 1)
m : ℕ
s : E
⊢ MeasurableSet {ω | (n + 1, ω) ∈ ⇑(StronglyMeasurable.approx h𝓕 m) ⁻¹' {s}}

Tactic:
apply measurableSet_prodMk_add_one_of_predictable

Goal state after:
case refine_1
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := ⋯
this : MeasurableSpace Ω := ⋯
X : ℕ → Ω → E := ⋯
m : ℕ
s : E
⊢ MeasurableSet (⇑(StronglyMeasurable.approx h𝓕 m) ⁻¹' {s})
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
⊢ Martingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_⟩
  calc μ[g j | ℱ i] =ᵐ[μ] μ[f j | ℱ i] := (condExp_congr_ae (h_eq j)).symm
    _ =ᵐ[μ] g i := (hf.2 i j hij).trans (h_eq i)

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

Goal state before:
pp: Ω : 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))
⊢ IsStronglyPredictable 𝓕 u

Tactic:
by
  let : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
  -- first layer of approximation
  let X m (x : ℕ × Ω) := match x.1 with
    | 0 => h₀.approx m x.2
    | n + 1 => (h n).approx m x.2
  -- second layer of approximation (to ensure the whole process has finite range)
  let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩
  refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
  · intro s
    rw [(by aesop : Y m ⁻¹' {s} = ⋃ n : ℕ, {n} ×ˢ ((Function.curry (Y m) n) ⁻¹' {s}))]
    refine MeasurableSet.iUnion <| fun n ↦ ?_
    rcases n with rfl | n
    · apply measurableSet_predictable_singleton_bot_prod
      let : MeasurableSpace Ω := 𝓕 0
      exact (h₀.approx m).measurableSet_fiber s
    · apply measurableSet_predictable_singleton_prod
      by_cases! hmk : n + 1 ≤ m
      · rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]
        let : MeasurableSpace Ω := 𝓕 n
        exact ((h n).approx m).measurableSet_fiber s
      · rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) 0)]
        apply 𝓕.mono (i := 0) (by simp)
        let : MeasurableSpace Ω := 𝓕 0
        exact (h₀.approx m).measurableSet_fiber s
  · apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
    · refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)
      rcases n with rfl | n
      · exact @(h₀.approx m).finite_range
      · exact @((h n).approx m).finite_range
    · intro e he
      obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he
      simp_rw [Set.mem_iUnion, Set.mem_range]
      exact ⟨if n ≤ m then n else 0, by aesop, ω, by aesop⟩
  · intro ⟨n, ω⟩
    rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]
    · rcases n with rfl | n
      · exact h₀.tendsto_approx ω
      · exact (h n).tendsto_approx ω
    · filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

Tactic:
simp only [upperCrossingTime_succ_eq]

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case neg.refine_2
Ω : 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
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
this : ⊥ ≤ ↑k → f (↑k) ω ∉ Set.Ici r
⊢ f (k + 1) ω - r ≤ ↑R

pp: case neg.refine_1
Ω : 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
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ ↑k < leastGE f r ω

Tactic:
· simp only [bot_eq_zero, zero_le, Set.mem_Ici, not_le, forall_const] at this
    exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))

Goal state after:
case neg.refine_1
Ω : 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
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ ↑k < leastGE f r ω
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
this : Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
rwa [iSup_singleton] at this

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
j : WithTop ι
⊢ MeasurableSet ((fun a ↦ τ (↑a).2) ⁻¹' Set.Iic j)

Tactic:
cases j with

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

Goal state before:
pp: case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)

Tactic:
exact ⟨-c, hc.neg⟩

Goal state after:
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 ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ω ∉ {ω | τ ω = ↑m}

Tactic:
simp only [Set.mem_ofPred_eq]

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 ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ¬τ ω = ↑m
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x ω : Ω
⊢ ω ∈ {a | ↑n + 1 ≤ τ a} ↔ ω ∈ {a | ↑n < τ a}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x ω : Ω
⊢ ↑n + 1 ≤ τ ω ↔ ↑n < τ ω
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
by simpa using ht_int_pos

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 ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω ↦ rexp (- -t * X ω)) μ

Tactic:
by simpa using ht_int_pos

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ limsup s atTop ↔ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

Tactic:
rw [← limsup_nat_add s 1,
    Set.limsup_eq_tendsto_sum_indicator_atTop (zero_lt_one (α := ℝ)) (fun n ↦ s (n + 1))]
  exact tendsto_sum_indicator_atTop_iff' hs

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
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (z : F), ⟪u, z - L (∫ (x : E), x ∂μ)⟫ * ⟪v, z - L (∫ (x : E), x ∂μ)⟫ ∂Measure.map (⇑L) μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ

Tactic:
integral_map

Goal state after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (x : E), ⟪u, L x - L (∫ (x : E), x ∂μ)⟫ * ⟪v, L x - L (∫ (x : E), x ∂μ)⟫ ∂μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ

case hφ
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

case hfm
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable (fun z ↦ ⟪u, z - L (∫ (x : E), x ∂μ)⟫ * ⟪v, z - L (∫ (x : E), x ∂μ)⟫) (Measure.map (⇑L) μ)
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 μ
x y : E
⊢ ⟪∫ (y : E), ⟪x, y⟫ • y ∂μ, y⟫ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y

Tactic:
rw [real_inner_comm, ← integral_inner]

Goal state after:
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 μ
x y : E
⊢ ∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y

case hf
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 μ
x y : E
⊢ Integrable (fun y ↦ ⟪x, y⟫ • y) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₁ x‖ ≤ ‖L₁‖ * ‖x‖

pp: case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖

Tactic:
· exact ContinuousLinearMap.le_opNorm L₁ x

Goal state after:
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖
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
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
⊢ ∫ (x : E), ∫ (y : E), L x + L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ ∂μ =
    ∫ (x : E), L x + ∫ (y : E), L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ ∂μ

Tactic:
by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]

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

Goal state before:
pp: I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f; projectiveFamily I] = Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
rw [projectiveFamily, variance_map_equiv]
  rfl

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Measure.map (fun x ↦ x.ofLp i) (multivariateGaussian μ S) = gaussianReal (μ.ofLp i) (S i i).toNNReal

Tactic:
← EuclideanSpace.coe_proj,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Measure.map (⇑(EuclideanSpace.proj i)) (multivariateGaussian μ S) = gaussianReal (μ.ofLp i) (S i i).toNNReal