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

Goal state before:
pp: case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (k + 1) = ↑p / ↑(m ^ (k + 1)!)

Tactic:
rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity

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

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x

Tactic:
add_int_iff

Goal state after:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ volume (B a b) = ↑(2 / ↑b ^ r)

Tactic:
Real.volume_ball,

Goal state after:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ENNReal.ofReal (2 * (1 / ↑b ^ r)) = ↑(2 / ↑b ^ r)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
⊢ False

Tactic:
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| := by
    intro b hb
    replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
    have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) := by
      simp only [one_div]
      exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
    refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
    exact fun m hm a => hm a

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
obtain ⟨b, hb, hb'⟩ := h a ha

Goal state after:
case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ b, IsCompl ⟨a, ha⟩ b
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s✝ : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x✝ : Concept α β r
hc : x✝ ∈ upperBounds s
⊢ sSup s ≤ x✝

Tactic:
exact intent_subset_intent_iff.1 <|
        subset_iInter₂ fun a ha ↦ intent_subset_intent_iff.2 (hc ha)

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (sInf (range fun i ↦ f i)).intent = upperPolar r (⋂ i, (f i).extent)

Tactic:
intent_sInf,

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ upperPolar r (⋂ i ∈ range fun i ↦ f i, i.extent) = upperPolar r (⋂ i, (f i).extent)
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S

Tactic:
· apply h.1 (Or.inr ⟨refl _, refl _⟩)

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
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)
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
⊢ E =ᵐ[volume] ∅ ∨ E ∈ ae volume

Tactic:
← eventuallyEq_univ

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)
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
⊢ E =ᵐ[volume] ∅ ∨ E =ᵐ[volume] univ
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ⨆ b ∈ Subtype.val '' s, ↑a ⊓ b ≤ sSup (Subtype.val '' range fun x ↦ a ⊓ ↑x)

Tactic:
sSup_image,

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ⨆ b ∈ Subtype.val '' s, ↑a ⊓ b ≤ ⨆ a_1 ∈ range fun x ↦ a ⊓ ↑x, ↑a_1
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : 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, P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x

Tactic:
by
  classical
  set f : α → α := fun a ↦ if ha : a ∈ u then
    (if hb : ∃ b : t, P.Rel a b then f₀ hb.choose else P.rep (P.partOf_mem ha)) else a with hfdef
  refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
  · simp only [hfdef, ha, ↓reduceDIte]
    split_ifs with h
    · exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem
    push Not at h
    exact P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)
  · simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]
    split_ifs with h₁ h₂ h₂
    · exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec
    · exact h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim
    · exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim
    congr 1
    rwa [← rel_iff_partOf_eq_partOf_of_mem _ hab.left_mem hab.right_mem]
  obtain (ha | ha) := em (a.1 ∈ u) |>.symm
  · simp [hfdef, ha, h_notMem _ ha]
  simp only [hfdef, ha, ↓reduceDIte]
  split_ifs with h
  · exact h_eq _ _ h.choose_spec |>.symm
  exact h ⟨a, rel_rfl_iff.mpr ha⟩ |>.elim

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ 𝓕.predictable ≤ MeasurableSpace.map (fun p ↦ (↑p.1, p.2)) (Subtype.instMeasurableSpace.prod (↑𝓕 n))

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ ∀ t ∈ {s | ∃ A, MeasurableSet A ∧ s = {⊥} ×ˢ A} ∪ {s | ∃ i A, MeasurableSet A ∧ s = Set.Ioi i ×ˢ A}, MeasurableSet t
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
⊢ 𝓕.predictable ≤ m'

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
⊢ ∀ t ∈ {s | ∃ A, MeasurableSet A ∧ s = {⊥} ×ˢ A} ∪ {s | ∃ i A, MeasurableSet A ∧ s = Set.Ioi i ×ˢ A}, MeasurableSet t
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f + g) ℱ μ

Tactic:
refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
  refine EventuallyLE.trans ?_ (condExp_add (hf.integrable j) (hg.integrable j) _).symm.le
  filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]
  intros
  refine add_le_add ?_ ?_ <;> assumption

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

Goal state before:
pp: case refine_3.succ
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
ω : Ω
n : ℕ
⊢ Tendsto (fun m ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))

Tactic:
exact (h n).tendsto_approx ω

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 β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Tactic:
change j ∈ {i | u i ω ∈ s} at hj₂

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m
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ω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω

Tactic:
conv_rhs => rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]

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ω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
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✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f i - f (i + 1) | ↑𝒢 i]
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg

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✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f i - f (i + 1) | ↑𝒢 i]
⊢ ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[(-f) (i + 1) - (-f) i | ↑𝒢 i]
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

Tactic:
· rw [not_lt] at hN'
    exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

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

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω < i

Tactic:
· obtain ⟨k, hk₁, hk₂⟩ := h'
    refine lt_of_le_of_lt ?_ hk₁.2
    exact hittingBtwn_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂

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

Goal state before:
pp: case neg
Ω : 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
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi' : ¬i ≤ m₁
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ i

Tactic:
change j ∈ {i | u i ω ∈ s} at hj₂

Goal state after:
case neg
Ω : 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₁
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi' : ¬i ≤ m₁
hj₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ∀ (i : ι), t < i → ⨅ m_1, ↑f (s m_1) ≤ ↑f i

Tactic:
intro i hti

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
i : ι
hti : t < i
⊢ ⨅ m_1, ↑f (s m_1) ≤ ↑f i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ 0 ≤ᵐ[μ] fun a_1 ↦ (b - a) * ↑(upcrossingsBefore a b f N a_1)

pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (fun a_1 ↦ (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᵐ[μ]
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)

Tactic:
· exact Eventually.of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)

Goal state after:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (fun a_1 ↦ (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᵐ[μ]
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m ↦ eLpNorm μ[f m - g | ↑ℱ n] 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
x : Ω
hx : μ[f m | ↑ℱ n] x = f n x
⊢ (μ[f m | ↑ℱ n] - μ[g | ↑ℱ n]) x = (f n - μ[g | ↑ℱ n]) x

Tactic:
simp only [hx, Pi.sub_apply]

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

Goal state before:
pp: Ω : 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]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
x : Ω
hx : μ[g | ↑ℱ n] x = μ[limitProcess (fun i ↦ μ[g | ↑ℱ i]) ℱ μ | ↑ℱ n] x
a✝ : x ∈ s
⊢ μ[g | ↑ℱ n] x = μ[limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ | ↑ℱ n] x

Tactic:
rw [hx]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
refine le_antisymm ?_ ?_
  · exact le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
      (measurableSpace_mono _ hπ fun _ => min_le_right _ _)
  · intro s
    change MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s →
      MeasurableSet[(hτ.min hπ).measurableSpace] s
    simp_rw [IsStoppingTime.measurableSet]
    have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by
      intro i; ext1 ω; simp
    simp_rw [this, Set.inter_union_distrib_left]
    exact fun h ↦ ⟨h.1.1, fun i ↦ (h.left.2 i).union (h.right.2 i)⟩

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

pp: case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
· intro u v _ huint hvint hu hv hu_eq hv_eq
    rw [memLp_one_iff_integrable] at huint hvint
    rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]

Goal state after:
case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
apply Integrable.of_mem_Icc (exp (min (a * t) (b * t))) (exp (max (a * t) (b * t)))
  · exact (measurable_exp.comp_aemeasurable (hm.const_mul t))
  filter_upwards [hb] with ω ⟨hl, hr⟩
  simp only [Set.mem_Icc, exp_le_exp, inf_le_iff, le_sup_iff]
  by_cases ht : 0 ≤ t
  · exact ⟨Or.inl (by nlinarith), Or.inr (by nlinarith)⟩
  · exact ⟨Or.inr (by nlinarith), Or.inl (by nlinarith)⟩

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

Goal state before:
pp: case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * x)

Tactic:
simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]

Goal state after:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ 0 ≤ |t| * x