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

Goal state before:
pp: p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r

Tactic:
simp [← div_mul_div_comm, ← r.cast_def, mul_comm]

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

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x * ↑r - ↑(r.num * m) / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p

Tactic:
rw [A, ← sub_mul, abs_mul]
    simp only [smul_eq_mul, id, Nat.cast_mul]
    calc _ < C / ↑n ^ p * |↑r| := by gcongr
      _ = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p := ?_
    rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
    · simp only [Rat.cast_abs]
    all_goals positivity

Goal state after:
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
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)
⊢ NullMeasurableSet E μ

Tactic:
refine (MeasurableSet.measurableSet_blimsup fun n hn =>
      IsOpen.measurableSet ?_).nullMeasurableSet

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
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)
n : ℕ
hn : 0 < n
⊢ IsOpen (approxAddOrderOf 𝕊 n (δ n))
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
⊢ sInf s ≤ e

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : e ∈ lowerBounds s
⊢ e ≤ sInf s

Tactic:
· by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (sInf_apply_le he ha.1)

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : e ∈ lowerBounds s
⊢ e ≤ sInf s
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ sSup A.left ≤ x✝ ↔ x✝ ∈ A.right

Tactic:
sSup_le_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ x✝ ∈ A.right
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent
h : ∀ b ∈ upperBounds (⇑f '' B.left), sSup (⇑f '' A.left) ≤ b
⊢ x ∈ lowerBounds B.right

Tactic:
sSup_le_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent
h : ∀ b ∈ upperBounds (⇑f '' B.left), ∀ b_1 ∈ ⇑f '' A.left, b_1 ≤ b
⊢ x ∈ lowerBounds B.right
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a < b
⊢ ∃ c, a ≤ principal c ∧ principal c < b

Tactic:
rw [← intent_ssubset_intent_iff, Set.ssubset_iff_exists] at h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r ∈ c, r x z

Tactic:
have : IsPartialOrder _ _ := hc₁ h₁s₂

Goal state after:
case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ ∃ r ∈ c, r x z
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y

Tactic:
have : IsPartialOrder _ _ := hc₁ h₁s₂

Goal state after:
case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ x = y
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
o : Ordinal.{u}
h : o ≤ rank r a
⊢ o ∈ Set.range (rank r)

Tactic:
by
  obtain ⟨b, hb, rfl⟩ := Acc.mem_range_rank_of_le (hwf.apply r a) h
  exact ⟨b, rfl⟩

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h

Tactic:
by
  simp only [biUnion_eq_iUnion]
  exact EventuallyLE.cardinal_iUnion hS fun i => h i i.2

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∃ n, ∀ t ⊆ s, t.encard = ↑n → ¬IsChain r t

Tactic:
obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp h

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight r
⊢ ∃ n, ∀ t ⊆ s, t.encard = ↑n → ¬IsChain r t
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, #↑i < c ∧ iᶜ ⊆ s
_t : Set α
htf : #↑_t < c
hts : _tᶜ ⊆ s
⊢ s ∈ cocardinal α hreg

Tactic:
by
      have : #↑sᶜ < c := by
        apply lt_of_le_of_lt _ htf
        rw [compl_subset_comm] at hts
        apply Cardinal.mk_le_mk_of_subset hts
      simp_all only [mem_cocardinal]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
b : α
n : ℕ
hb : 0 ≤ b
⊢ ↑n ∈ Set.Iic b ↔ n ∈ Finset.Iic ⌊b⌋₊

Tactic:
simp [le_floor_iff hb]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

Tactic:
· exact @mem_compl_of_ge _ _ _

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ⊓ xᶜ ∈ I

Tactic:
inf_compl_eq_bot

Goal state after:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ ⊥ ∈ I
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t

Tactic:
obtain ⟨t, ht, hxt⟩ := hx

Goal state after:
α : Type u_1
x : α
u : Set α
P : Partition u
t : Set α
ht : t ∈ ↑P
hxt : x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Module: Mathlib.Order.TeichmullerTukey

Goal state before:
pp: α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
cne : c.Nonempty
s : Set α
sc : s ⊆ ⋃₀ c
sfin : s.Finite
t : Set α
tc : t ∈ c
st : s ⊆ t
⊢ s ∈ F

Tactic:
exact (hF t).mp (cF tc) s st sfin

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
r : SubRootedTree t
hr : r ∈ t.subtrees
⊢ r.root ≠ ⊥

Tactic:
simp only [RootedTree.subtrees, Set.mem_ofPred_eq] at hr
  exact hr.1

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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f - martingalePart (f + g) ℱ μ) n ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω

Tactic:
Pi.sub_apply

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✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n : ℕ
⊢ StronglyMeasurable (MeasureTheory.upcrossingStrat a b f N n)

Tactic:
change StronglyMeasurable[ℱ n] fun ω =>
    ∑ k ∈ Finset.range N, ({n | lowerCrossingTime a b f N k ω ≤ n} ∩
      {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n : ℕ
⊢ StronglyMeasurable fun ω ↦
    ∑ k ∈ Finset.range N,
      ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
convert! notMem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab) using 1

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

Goal state before:
pp: case ht
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j, n ≤ j ∧ u j ω ∈ F
hE : ∃ j, n ≤ j ∧ u j ω ∈ E
⊢ BddBelow {j | n ≤ j ∧ u j ω ∈ F}

Tactic:
exact ⟨n, by simp only [mem_lowerBounds]; 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 : ι
⊢ Monotone fun x ↦ hittingBtwn u s n x ω

Tactic:
intro m₁ m₂ hm
  by_cases h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
  · exact (hittingBtwn_eq_hittingBtwn_of_exists hm h).le
  · simp_rw [hittingBtwn, if_neg h]
    split_ifs with h'
    · 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⟩
    · exact hm

Goal state after:
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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ sInf (Set.Icc n' m ∩ {i | u i ω ∈ s})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ m

Tactic:
· have ⟨t, ht⟩ := h_n'
    exact absurd ⟨t, ⟨hnn'.trans ht.1.1, ht.1.2⟩, ht.2⟩ h_n

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ m
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet (⋂ n ∈ s, {ω | ↑i ≤ τ n ω})

pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ {ω | ⨅ n ∈ s, τ n ω < ↑i}ᶜ = ⋂ n ∈ s, {ω | ↑i ≤ τ n ω}

Tactic:
· exact MeasurableSet.biInter hs <| fun n hn ↦ (hτ n hn).measurableSet_ge i

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst✝ : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ {ω | ⨅ n ∈ s, τ n ω < ↑i}ᶜ = ⋂ n ∈ s, {ω | ↑i ≤ τ n ω}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0
⊢ upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 1 - 1 + 0

Tactic:
Nat.add_succ_sub_one,

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0
⊢ upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 0 + 0
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case compl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω) in tᶜ, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl,

Goal state after:
case compl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω) in tᶜ, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ.trim hle
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : StronglyAdapted ℱ f
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N

Tactic:
by
    filter_upwards with ω
    rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]
    exact upcrossingsBefore_le _ _ hab

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

Goal state before:
pp: case compl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
    have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
      (hlimint.trim hle stronglyMeasurable_limitProcess)
    rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]

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

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by
      rw [Set.inter_assoc, Set.inter_self]
    rw [this]
    exact measurableSet_inter_le _ hπ _ h

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ mgf X 0 = 0

Tactic:
by ext; simp [mgf]

Goal state after: