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

Goal state before:
pp: Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
⊢ ∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)

Tactic:
have me0 : 0 < max (1 / ε) M := lt_max_iff.mpr (Or.inl (one_div_pos.mpr e0))
  -- The maximum between `1 / ε` and `M` works
  refine ⟨max (1 / ε) M, me0, fun z a => ?_⟩
  -- First, let's deal with the easy case in which we are far away from `α`
  by_cases dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M
  · exact one_le_mul_of_one_le_of_one_le (d0 a) dm1
  · -- `j z a = z / (a + 1)`: we prove that this ratio is close to `α`
    have : j z a ∈ closedBall α ε := by
      refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
      exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le
    -- use the "separation from `1`" (assumption `L`) for numerators,
    refine (L this).trans ?_
    -- remove a common factor and use the Lipschitz assumption `B`
    gcongr
    · exact zero_le_one.trans (d0 a)
    · refine (B this).trans ?_
      gcongr
      apply le_max_right

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < 1 / A

pp: case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
· refine (lt_div_iff₀' hA).mpr ?_
    refine lt_of_le_of_lt ?_ a1
    gcongr
    refine hn.le.trans ?_
    rw [one_add_one_eq_two]
    gcongr
    norm_cast

Goal state after:
case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)

Tactic:
have : ∀ᶠ n : ℕ in atTop, C < n ^ (p - q) := by
    simpa only [(· ∘ ·), neg_sub, one_div] using
      ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_natCast_atTop_atTop).eventually
        (eventually_gt_atTop C)

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 < x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 ≤ x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 ↦ x1 ≤ x2) s
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.left
y : α
hy : y ∈ A.right
⊢ f x ≤ f y

Tactic:
exact hf <| rel_extent_intent hx hy

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case neg
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
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
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
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∃ p, ¬A ↑p =ᵐ[μ] ∅ ∨ ¬B ↑p =ᵐ[μ] ∅
⊢ E =ᵐ[volume] ∅ ∨ E =ᵐ[volume] univ

Tactic:
right

Goal state after:
case neg
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
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∃ p, ¬A ↑p =ᵐ[μ] ∅ ∨ ¬B ↑p =ᵐ[μ] ∅
⊢ E =ᵐ[volume] univ
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
s : Set α
⊢ s ∈ cocountable ↔ sᶜ.Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, mem_cocardinal, lt_aleph_one_iff]

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

Goal state before:
pp: a b : ℕ
⊢ (Ioo a b).ncard = b - a - 1

Tactic:
by
  simpa [← Set.ncard_coe_finset] using Nat.card_Ioo a b

Goal state after:
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)
this : ¬Pairwise (Disjoint on B)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_2.inl
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ g i ≤ g j

Tactic:
exact hfg.symm hi hj h

Goal state after:
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
αs : Type u_1 := (i : ℕ) × α i
x✝² : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
x✝¹ : αs
i : ℕ
a : α i
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ ⟨i + 1, π ⋯ b⟩ = ⟨j, b⟩

Tactic:
by cases hj; rw [π_refl]

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

Goal state before:
pp: case refine_2
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
⊢ (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯) = if hb : ∃ b_1, P.Rel b ↑b_1 then f₀ hb.choose else P.rep ⋯

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = f₀ h₂.choose

case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯

case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥

Tactic:
simp only [Nat.add_sub_cancel_right, ← Function.iterate_succ_apply', Nat.succ_eq_add_one]

Goal state after:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[n✝ + 1] r = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ False

Tactic:
have : t₁.root ≤ (v₁ : t) ⊓ (v₂ : t) := by
      simp only [le_inf_iff]
      exact ⟨h₁, nh ▸ h₂⟩

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ v₁ ⊓ v₂
⊢ False
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α + 0 = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]
      exact (OrderIso.sumLexEmpty (β := PEmpty) (α := α)).type_congr

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 : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
c : ℝ
n : ℕ
⊢ predictablePart (c • f) ℱ μ n =ᵐ[μ] c • predictablePart f ℱ μ n

Tactic:
simp only [predictablePart, Finset.smul_sum]
  refine eventuallyEq_sum fun i hi => ?_
  simp [← smul_sub, condExp_smul]

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

Goal state before:
pp: case pos.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ n ≤ b

Tactic:
Set.mem_inter_iff

Goal state after:
case pos.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∧ b ∈ {i | u i ω ∈ s}
⊢ n ≤ b
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 ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
Set.mem_inter_iff

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∧ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
hl : MeasurableSet {ω | (fun ω ↦ ↑(lowerCrossingTime a b f N i ω)) ω ≤ ↑n}
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (i + 1) ω}) n

Tactic:
have hu := hf.isStoppingTime_upperCrossingTime (a := a) (b := b) (N := N) (n := i + 1) n

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
hl : MeasurableSet {ω | (fun ω ↦ ↑(lowerCrossingTime a b f N i ω)) ω ≤ ↑n}
hu : MeasurableSet {ω | (fun ω ↦ ↑(upperCrossingTime a b f N (i + 1) ω)) ω ≤ ↑n}
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (i + 1) ω}) n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case ht
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ BddBelow (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

pp: case hs
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ (Set.Icc n m₁ ∩ {i | u i ω ∈ s}).Nonempty

Tactic:
exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩]

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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
refine csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_
    by_contra hnN
    exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)

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

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

Tactic:
exact f ⊥

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

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

Tactic:
exact f ⊥

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

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

Tactic:
rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
h :
  ↑ε * μ.real {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a} ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x ∂μ
⊢ ε • (μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}).toReal ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

case ha
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
h :
  ↑ε * μ.real {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a} ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x ∂μ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≠ ∞

case hb
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
h :
  ↑ε * μ.real {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a} ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x ∂μ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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}
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)

Tactic:
have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)

Goal state after:
Ω : 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
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ μ[(s j).indicator fun x ↦ 1 | ↑(filtrationOfSet hsm) i] =ᵐ[μ] fun x ↦ μ.real (s j)

Tactic:
Filtration.filtrationOfSet_eq_natural (β := fun _ ↦ ℝ) hsm

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ μ[(s j).indicator fun x ↦ 1 | ↑(Filtration.natural (fun i ↦ (s i).indicator fun x ↦ 1) ⋯) i] =ᵐ[μ] fun x ↦
    μ.real (s j)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
a✝ : stoppedValue u τ ω ∈ t
h : ¬τ ω = ⊤
⊢ (∃ x, τ ω ≤ ↑(seq x)) ∨ τ ω = ⊤

Tactic:
· lift τ ω to ι using h with t
      simp only [coe_le_coe, coe_ne_top, or_false]
      rw [tendsto_atTop] at h_seq_tendsto
      exact (h_seq_tendsto t).exists

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

Goal state before:
pp: case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ x ∉ {a | τ a = ↑n} ∩ {a | ↑n + 1 ≤ τ a}

Tactic:
· rintro ⟨h₁, h₂⟩
      rw [Set.mem_ofPred] at h₁ h₂
      rw [h₁] at h₂
      norm_cast at h₂
      grind

Goal state after:
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) (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
by
  rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
  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: