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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
⊢ ¬Pairwise (Disjoint on B)

Tactic:
by_contra h

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ False
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
h'' : ∀ (j : ↑(Icc 0 n)), (B j).Nonempty
⊢ n = 0

Tactic:
simpa using subsingleton_of_disjoint_isClosed_iUnion_eq_univ h'' h hB h'

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

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r b c

Tactic:
suffices r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c)) by
    simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this
  apply (h₄ (inf_le_of_left_le hbd) _).1
  simpa [sup_eq_right.mpr (le_inf hab hac), sup_eq_left.mpr (inf_le_of_left_le hbd)] using
    ((h₄ (le_trans hab hbd) had).2 : r (a ⊔ b ⊓ c) (d ⊔ b ⊓ c))

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
have IinS : ↑I ∈ S := ⟨Order.Ideal.isIdeal I, by trivial⟩

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
by
  set αs := (i : ℕ) × α i
  let _ : PartialOrder αs := {
    le := fun a b ↦ ∃ h, π h b.2 = a.2
    le_refl := fun a ↦ ⟨rfl.le, π_refl _⟩
    le_trans := fun _ _ c h h' ↦ ⟨h.1.trans h'.1, by rw [← π_trans h.1 h'.1 c.2, h'.2, h.2]⟩
    le_antisymm := by grind }
  have hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.1 + 1 = b.1 := by
    simp only [αs, covBy_iff_lt_and_eq_or_eq, lt_iff_le_and_ne, ne_eq, Sigma.forall, and_assoc,
      and_congr_right_iff, or_iff_not_imp_left]
    rintro i a j b ⟨h : i ≤ j, rfl : π h b = a⟩
    refine ⟨fun ⟨hne, h'⟩ ↦ ?_, ?_⟩
    · have hle' : i + 1 ≤ j := h.lt_of_ne <| by rintro rfl; simp [π_refl] at hne
      exact congr_arg Sigma.fst <| h' (i + 1) (π hle' b) ⟨by simp, by rw [π_trans]⟩ ⟨hle', by simp⟩
        (fun h ↦ by simp at h)
    rintro rfl
    refine ⟨fun h ↦ by simp at h, ?_⟩
    rintro j c ⟨hij : i ≤ j, hcb : π _ c = π _ b⟩ ⟨hji : j ≤ i + 1, rfl : π hji b = c⟩ hne
    replace hne := show i ≠ j by rintro rfl; contradiction
    obtain rfl := hji.antisymm (hij.lt_of_ne hne)
    rw [π_refl]
  have : IsStronglyAtomic αs := by
    simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨⟨hij : i ≤ j, h2 : π hij b = a⟩, hne⟩
    have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)
    exact ⟨⟨_, π hle b⟩, ⟨⟨by simp, by rw [π_trans, ← h2]⟩, by simp⟩, ⟨hle, by simp⟩⟩
  obtain ⟨a₀, ha₀, ha₀inf⟩ : ∃ a₀ : αs, a₀.1 = 0 ∧ (Ici a₀).Infinite := by
    obtain ⟨a₀, ha₀⟩ := Finite.exists_infinite_fiber (fun (a : αs) ↦ π zero_le a.2)
    refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩
    simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]
    exact fun i x h ↦ ⟨zero_le, h⟩
  have hfin : ∀ (a : αs), {x | a ⋖ x}.Finite := by
    refine fun ⟨i, a⟩ ↦ ((hfin i a).image (fun b ↦ ⟨_, b⟩)).subset ?_
    simp only [αs, hcovby, subset_def, mem_ofPred_eq, mem_image, and_imp, Sigma.forall]
    exact fun j b ⟨_, _⟩ hj ↦ ⟨π hj.le b, by rwa [π_trans], by cases hj; rw [π_refl]⟩
  obtain ⟨f, hf0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite hfin ha₀inf
  have hr : ∀ i, (f i).1 = i :=
    Nat.rec (by rw [hf0, ha₀]) (fun i ih ↦ by rw [← (hcovby.1 (hf i)).2, ih])
  refine ⟨fun i ↦ by rw [← hr i]; exact (f i).2, fun i j hij ↦ ?_⟩
  convert! (f.monotone hij).2 <;>
  simp [hr]

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

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P : Partition s
hxP : x ∈ P
⊢ s ≠ ⊥

Tactic:
by
  rintro rfl
  exact P.notMem_of_bot _ hxP

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_3
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f x b

Tactic:
trans f a b
    · -- f a y ≤ f a b
      rw [← h]
      apply le_iSup₂ y hy
    · -- f a b ≤ f x b
      rw [← h']
      apply iInf₂_le x hx

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

Goal state before:
pp: case inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ f (f a) = f a

Tactic:
rw [eq_comm, hf.apply_eq_apply_iff_rel ha]
    exact hf.rel_apply ha

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

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ Equiv.ulift.symm x✝¹ ≤ Equiv.ulift.symm x✝ ↔ x✝¹ ≤ x✝

Tactic:
by
  simp only [ulift_symm_apply, ULift.up_le]

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
⊢ sInf {s | ⊤ ≤ ↑s} = ⊤

Tactic:
refine le_antisymm le_top ?_

Goal state after:
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
⊢ ⊤ ≤ sInf {s | ⊤ ≤ ↑s}
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (α ⊕ₗ PEmpty.{u + 1}) = type α

Tactic:
exact (OrderIso.sumLexEmpty (β := PEmpty) (α := α)).type_congr

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

Goal state before:
pp: a b c : OrderType.{u_1}
x✝⁵ : Type u_1
x✝⁴ : LinearOrder x✝⁵
x✝³ : Type u_1
x✝² : LinearOrder x✝³
x✝¹ : Type u_1
x✝ : LinearOrder x✝¹
⊢ type x✝⁵ * (type x✝³ + type x✝¹) = type x✝⁵ * type x✝³ + type x✝⁵ * type x✝¹

Tactic:
simp only [← type_lex_prod, ← type_lex_sum]

Goal state after:
a b c : OrderType.{u_1}
x✝⁵ : Type u_1
x✝⁴ : LinearOrder x✝⁵
x✝³ : Type u_1
x✝² : LinearOrder x✝³
x✝¹ : Type u_1
x✝ : LinearOrder x✝¹
⊢ type (Lex ((x✝³ ⊕ₗ x✝¹) × x✝⁵)) = type (Lex (x✝³ × x✝⁵) ⊕ₗ Lex (x✝¹ × x✝⁵))
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
simp_rw [SetLike.ext'_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ ↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ ↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥
Module: Mathlib.Probability.Process.Predictable

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

Tactic:
rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
      · simp
      · ext p
        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
          iff_false, not_and]
        rw [p.1.2]
        grind

Goal state after:
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 : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
by_contra h

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
⊢ False
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : hittingBtwn u s n m ω ≤ i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
exact ⟨hittingBtwn u s n m ω, ⟨le_hittingBtwn_of_exists h_exists, h'⟩,
      hittingBtwn_mem_set h_exists⟩

Goal state after:
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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
⊢ ∃ j ∈ Set.Icc n m, u j ω ∈ s

Tactic:
by_contra h

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False
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✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale (fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

Tactic:
have hξbdd : ∀ i, ∃ C, ∀ ω, ‖ξ i ω‖ ≤ C := fun i =>
    ⟨R, fun ω => (abs_of_nonneg (hnonneg i ω)).trans_le (hbdd i ω)⟩

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✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), ‖ξ i ω‖ ≤ C
⊢ Submartingale (fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe.coe
Ω : 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 π
j : ι
ω : Ω
a b : ι
⊢ ↑a + ↑b ≤ ↑j ↔ ∃ i, ↑b = ↑↑i ∧ ↑a + ↑↑i ≤ ↑j

Tactic:
| coe b =>

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]
  rw [integral_sub h_int (integrable_const _)]
  simp only [sub_mul, integral_const, smul_eq_mul, one_mul]

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

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

Tactic:
abs_of_nonpos hu

Goal state after:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (-u * X ω)) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
refine .of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_
  filter_upwards [hb] with ω hb
  exact ⟨by positivity, by gcongr⟩

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | τ a = ↑n} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x

Tactic:
@eq_comm _ _ (n : WithTop ℕ),

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | ↑n = τ a} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : 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 hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
    exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ (gaussianReal μ v) Set.univ = 1

Tactic:
by_cases h : v = 0 <;> simp [gaussianReal_of_var_ne_zero, h]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ ℙ.withDensity (gaussianPDF μ v)

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Goal state after:
case refine_1
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ AEMeasurable (gaussianPDF μ v) ℙ

case refine_2
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (ℙ.withDensity fun x ↦ ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
exact f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

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

Goal state before:
pp: case neg.e_f
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * |c| = 1

Tactic:
rw [abs_inv, inv_mul_cancel₀]

Goal state after:
case neg.e_f
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c| ≠ 0
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
⊢ Measure.map X μ = Measure.map Y μ'

Tactic:
have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ x ≠ 0 :=
    DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
  apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
    continuous_inner (fun w ↦ ?_)
  rw [funext_iff] at h
  specialize h (Multiplicative.toAdd w * I)
  simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h
  simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
    RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]
  rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]

Goal state after:
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
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ∫ (x : E), ‖L₁ x‖ * ‖L₂ x‖ ∂μ ≤ ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ

Tactic:
refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)

Goal state after:
case refine_1
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 μ
⊢ Integrable (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) μ

case refine_2
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 μ
⊢ Integrable (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ

case refine_3
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
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) x
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < c.toReal / (1 - c).toReal

Tactic:
rw [one_lt_div_iff]

Goal state after:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
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 : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) ∂μ

Tactic:
refine setLIntegral_mono (by fun_prop) fun x hx ↦ ?_

Goal state after:
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 : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
x : E
hx : x ∈ closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
⊢ ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ≤ ENNReal.ofReal (rexp (C * t (n + 1) ^ 2))
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
this : NullSingletonClass (Measure.map (⇑L) μ)
⊢ (Measure.map (⇑L) μ) {L x} = 0

Tactic:
measure_singleton

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
this : NullSingletonClass (Measure.map (⇑L) μ)
⊢ 0 = 0
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
hL_zero : μ (⇑L ⁻¹' {L x}) = 0
⊢ μ {x} = 0

Tactic:
refine measure_mono_null ?_ hL_zero

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
hL_zero : μ (⇑L ⁻¹' {L x}) = 0
⊢ {x} ⊆ ⇑L ⁻¹' {L x}