mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
by
  rintro - ⟨a, ha, rfl⟩
  obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha
  replace hb : b ^ m ∈ {u : A | orderOf u = n} := by
    rw [← hb] at hmn ⊢; exact hmn.orderOf_pow
  apply ball_subset_thickening hb ((m : ℝ) • δ)
  convert! pow_mem_ball hm hab using 1
  simp only [nsmul_eq_mul, smul_eq_mul]

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j = (ConcreteCategory.hom (s.π.app { as := j })) t

Tactic:
rw [← w ⟨j⟩]

Goal state after:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j = (ConcreteCategory.hom (m ≫ (product f).π.app { as := j })) t
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : orderOf a * orderOf a ∣ orderOf b
hb : orderOf b = n
⊢ orderOf (a * b) = n

Tactic:
rwa [(Commute.all a b).orderOf_mul_eq_right_of_forall_prime_mul_dvd (orderOf_pos_iff.mp hn)
      fun p _ hp' => dvd_trans (mul_dvd_mul_right hp' <| orderOf a) han]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: case inl
α : Type u
a : α
r : α → α → Prop
ha : Acc r a
ho : ha.rank ≤ ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = ha.rank

Tactic:
exact ⟨a, ha, rfl⟩

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ Monotone (i.castSucc.succ.insertNth x f)

Tactic:
by
  rw [Fin.monotone_iff_le_succ]
  intro j
  obtain hj | rfl | hj := lt_trichotomy j i.castSucc
  · obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hj)
    grind [insertNth_apply_below, castPred_castSucc, hf j.castSucc_le_succ]
  · rwa [← succAbove_succ_self i.castSucc, insertNth_apply_succAbove, insertNth_apply_same]
  · obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hj)
    grind [insertNth_apply_same, insertNth_apply_above, hf j.castSucc_le_succ]

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty

Tactic:
constructor
  all_goals
  · intros
    by_contra! hh
    simp_all

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ StrictMono (i.castSucc.succ.insertNth x f)

Tactic:
rw [Fin.strictMono_iff_lt_succ] at hf ⊢
  intro j
  obtain hj | rfl | hj := lt_trichotomy j i.castSucc
  · obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hj)
    grind [insertNth_apply_below, castPred_castSucc]
  · rwa [← succAbove_succ_self i.castSucc, insertNth_apply_succAbove, insertNth_apply_same]
  · obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hj)
    grind [insertNth_apply_same, insertNth_apply_above]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : range ⇑m ⊆ range ⇑n
x : X
⊢ n x ≤ m x

Tactic:
by
    rw [← mem_range.mp (Set.range_subset_iff.mp h x)]
    exact n.monotone m.le_apply

Goal state after:
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
⊢ x ∈ Q

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

Tactic:
· obtain ⟨y, hy, hxy⟩ := hp h
      obtain ⟨x', hx', hyx'⟩ := hq hy
      obtain rfl := P.pairwiseDisjoint.eq_of_le h hx' (P.ne_bot_of_mem h) (hxy.trans hyx')
      rwa [hxy.antisymm hyx']

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

Goal state before:
pp: t : RootedTree
r : SubRootedTree t
⊢ ⊥ ∈ r ↔ r.root = ⊥

Tactic:
by
  simp [mem_iff]

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 g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : predictablePart (f + g) ℱ μ n ω = (predictablePart f ℱ μ n + predictablePart g ℱ μ n) ω
⊢ martingalePart (f + g) ℱ μ n ω = (martingalePart f ℱ μ n + martingalePart g ℱ μ n) ω

Tactic:
simp_all [martingalePart]

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : predictablePart (f + g) ℱ μ n ω = predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω
⊢ f n ω + g n ω - (predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω) =
    f n ω - predictablePart f ℱ μ n ω + (g n ω - predictablePart g ℱ μ n ω)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
hl : hittingAfter u s n ω ≠ ⊤
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
simp only [ne_eq, hittingAfter_eq_top_iff, not_forall, not_not] at hl

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
hl : ∃ x, ∃ (_ : n ≤ x), u x ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N n ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N n ω)

Tactic:
by
  induction n with
  | zero =>
    refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
  | succ k ih =>
    have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]
    refine ⟨this, fun n ↦ ?_⟩
    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
    simp [upperCrossingTime_le]

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
h_lt_eq_preimage : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iio ↑i
⊢ MeasurableSet (τ ⁻¹' Set.Iio ↑i)

Tactic:
h_Iio_eq_Union

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
h_lt_eq_preimage : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iio ↑i
⊢ MeasurableSet (τ ⁻¹' ⋃ j, {k | k ≤ ↑(seq j)})
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₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'
      refine le_csInf ⟨j, hj₁, hj₂⟩ ?_
      by_contra! ⟨i, hi₁, hi₂⟩
      exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ IsStoppingTime f (τ + π)

Tactic:
intro j
  have h : {ω | (τ + π) ω ≤ j} = ⋃ k : Set.Iic j, {ω | π ω = k} ∩ {ω | τ ω + k ≤ j} := by
    ext ω
    simp only [Pi.add_apply, Set.mem_ofPred_eq, Set.mem_iUnion, Set.mem_inter_iff]
    cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right
  exact h ▸ MeasurableSet.iUnion fun k => (hπ.measurableSet_eq_le k.2).inter (hτ.add_const' k.1 j)

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), f j x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
stoppedValue_piecewise_const,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), s.piecewise (f i) (f j) x ∂μ ≤ ∫ (x : Ω), f j x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ↑ε * μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ)

Tactic:
have hadd : ENNReal.ofReal (∫ ω, f n ω ∂μ) =
      ENNReal.ofReal
        (∫ ω in {ω | ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
          f 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
      exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn,
        integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ)
⊢ ↑ε * μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ)
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IsStoppingTime 𝒢 fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)

Tactic:
exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
⊢ c.toReal • ∫ (x : Ω), rexp (t * X x) ∂μ = c.toReal * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ

Tactic:
smul_eq_mul

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
⊢ c.toReal * ∫ (x : Ω), rexp (t * X x) ∂μ = c.toReal * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ s ∧ i < n

Tactic:
simp only [Set.mem_image, Finset.mem_coe, coe_eq_coe, exists_eq_right] at hbdd

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
h : ↑i < ↑n
hbdd : i ∈ s
⊢ i ∈ s ∧ i < n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : ↑t = τ ω
b : ℕ
hb : ↑b = π ω
hbdd : ↑b ≤ ↑N
⊢ untopA ↑t ≤ i ∧ i < untopA ↑b ↔ i ∈ {x ∈ Finset.range (N + 1) | ↑t ≤ ↑x ∧ ↑x < ↑b}

Tactic:
simp only [Nat.cast_le] at hbdd

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : ↑t = τ ω
b : ℕ
hb : ↑b = π ω
hbdd : b ≤ N
⊢ untopA ↑t ≤ i ∧ i < untopA ↑b ↔ i ∈ {x ∈ Finset.range (N + 1) | ↑t ≤ ↑x ∧ ↑x < ↑b}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : ↑t = τ ω
hbdd : ↑t ≤ ↑N
⊢ ↑t ∈ WithTop.some '' ↑(Finset.range (N + 1))

Tactic:
simp only [Nat.cast_le] at hbdd

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : ↑t = τ ω
hbdd : t ≤ N
⊢ ↑t ∈ WithTop.some '' ↑(Finset.range (N + 1))
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

Tactic:
have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin (mod_cast (hτ ω).trans hτn)

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ ↑n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
⊢ IsStoppingTime 𝒢 (s.piecewise τ η)

Tactic:
by
  intro n
  have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} := by
    ext1 ω
    simp only [Set.piecewise, Set.mem_ofPred_eq]
    by_cases hx : ω ∈ s <;> simp [hx]
  rw [this]
  by_cases hin : i ≤ n
  · have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
    exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))
  · have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin (mod_cast (hτ ω).trans hτn)
    have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin (mod_cast (hη ω).trans hηn)
    simp [hτn, hηn, @MeasurableSet.empty _ _]

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

Goal state before:

Tactic:
deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ HasLaw (-X) (gaussianReal (-μ) v) P

Tactic:
by
  rw [Pi.neg_def, ← Function.comp_def]
  exact HasLaw.comp ⟨by fun_prop, gaussianReal_map_neg⟩ hX

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

Goal state before:
pp: case convert_2
Ω : 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 μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0

Tactic:
exact hu 0 ⟨le_refl 0, le_of_lt ht⟩

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

Goal state before:
pp: 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
L : E ≃L[ℝ] F
⊢ IsGaussian (Measure.map (⇑L) μ) ↔ IsGaussian μ

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  suffices μ = (μ.map L).map L.symm by rw [this]; infer_instance
  rw [Measure.map_map (by fun_prop) (by fun_prop)]
  simp

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Var[⇑L; gaussianReal μ v] = ↑(L 1 ^ 2).toNNReal * ↑v

Tactic:
← variance_id_map,

Goal state after:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Var[id; Measure.map (⇑L) (gaussianReal μ v)] = ↑(L 1 ^ 2).toNNReal * ↑v

μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEMeasurable (⇑L) (gaussianReal μ v)
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
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ charFunDual μ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E) *
      charFunDual μ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E) =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E E) * charFunDual μ (L ∘SL ContinuousLinearMap.inr ℝ E E)

Tactic:
charFunDual_eq_of_forall_strongDual_eq_zero hμ,

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ cexp (-↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] / 2) *
      cexp (-↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 2) =
    cexp (-↑Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] / 2) *
      cexp (-↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 2)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
x : E
hxL₁ : ↑↑(MemLp.toLp (fun x ↦ L₁ x) ⋯) x = L₁ x
hxL₂ : ↑↑(MemLp.toLp (fun x ↦ L₂ x) ⋯) x = L₂ x
⊢ ↑↑(MemLp.toLp ⇑L₂ ⋯) x * ↑↑(MemLp.toLp ⇑L₁ ⋯) x = L₁ x * L₂ x

Tactic:
rw [hxL₁, hxL₂, mul_comm]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ cexp (↑(t • L m) * I - ↑(t • t • (f L) L) / 2) = cexp (↑t * ↑(L m) * I - ↑↑((f L) L).toNNReal * ↑t ^ 2 / 2)

Tactic:
smul_eq_mul

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ cexp (↑(t * L m) * I - ↑(t * (t * (f L) L)) / 2) = cexp (↑t * ↑(L m) * I - ↑↑((f L) L).toNNReal * ↑t ^ 2 / 2)