mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
⊢ ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W)

Tactic:
refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
k : Fin #t
⊢ (fun k ↦ W ↑(t.equivFin.symm k)) k ≠ ⊥

case refine_2
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
k : Fin #t
⊢ ∃ i, ↑((fun k ↦ W ↑(t.equivFin.symm k)) k) ⊆ ↑(U i)

case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)

case refine_4
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
⊢ Pairwise (Disjoint on fun k ↦ W ↑(t.equivFin.symm k))
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ a = 1 ∨ a = -1 ↔ a.y = 0

Tactic:
refine ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => ?_⟩

Goal state after:
d : ℤ
a : Solution₁ d
H : a.y = 0
⊢ a = 1 ∨ a = -1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
⊢ ↑q₁.num * ↑q₂.num - ↑d * (↑q₁.den * ↑q₂.den) = 0

Tactic:
rw [hq1, hq2, ← sq, ← sq]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
⊢ ↑q₂.num ^ 2 - ↑d * ↑q₂.den ^ 2 = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)

Tactic:
show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this : a.x * a₁.y ≤ a.y * a₁.x
⊢ d * a.y * (a.x * a₁.y) ≤ d * a.y * (a.y * a₁.x)

Tactic:
have := h.d_pos

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this✝ : a.x * a₁.y ≤ a.y * a₁.x
this : 0 < d
⊢ d * a.y * (a.x * a₁.y) ≤ d * a.y * (a.y * a₁.x)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < 1 + d * a.y ^ 2

Tactic:
have := h.d_pos

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this : 0 < d
⊢ 0 < 1 + d * a.y ^ 2
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}

Tactic:
ext j
  by_cases h₁ : j ∈ {beattySeq r k | k} <;> by_cases h₂ : j ∈ {beattySeq' s k | k}
  · exact (Set.not_disjoint_iff.2 ⟨j, h₁, h₂⟩ (Beatty.no_collision hrs)).elim
  · simp only [Set.mem_compl_iff, h₁, h₂, not_true_eq_false]
  · simp only [Set.mem_compl_iff, h₁, h₂, not_false_eq_true]
  · have ⟨k, h₁₁, h₁₂⟩ := (Beatty.hit_or_miss hrs.pos).resolve_left h₁
    have ⟨m, h₂₁, h₂₂⟩ := (Beatty.hit_or_miss' hrs.symm.pos).resolve_left h₂
    exact (Beatty.no_anticollision hrs ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩).elim

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ 0 < ∏ p ∈ d.primeFactors, s.nu p

Tactic:
by
      apply prod_pos
      intro p hpd
      have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
      have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
      exact s.nu_pos_of_prime p hp_prime hp_dvd

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ 1 < (inftyValuation K) X

Tactic:
rw [inftyValuation.X, ← log_lt_iff_lt_exp one_ne_zero, log_one]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ 0 < 1
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))

Tactic:
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]

Goal state after:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case prime
p : ℕ
hp : Prime p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
exact hp.sum_four_squares

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

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ partialSum (↑m) 0 = ↑1 / ↑(m ^ 0!)

Tactic:
by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
m✝ : R ⧸ p
c : R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext P

Goal state after:
case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
P✝ : Ideal S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
m✝ : R ⧸ p
c : R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
P : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ball (↑a / ↑b) (1 / ↑b ^ n) ∩ {x | Irrational x} ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
exact sdiff_subset_sdiff Subset.rfl (singleton_subset_iff.2 ⟨a / b, by norm_cast⟩)

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 p, ↑x = -1

Tactic:
conv =>
    congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
  rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (a⁻¹ * b) = n

Tactic:
← orderOf_inv,

Goal state after:
case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (a⁻¹ * b)⁻¹ = n
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 : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact (cardinal_iInter_mem hS).trans Subtype.forall

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ r.core (x✝ ∩ y✝) ∈ l

Tactic:
convert! inter_mem hs ht

Goal state after:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ r.core (x✝ ∩ y✝) = r.core x✝ ∩ r.core y✝
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a ↦ exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t ↦ Nat.rec ⟨b, hb⟩ (fun x a ↦ ⟨⋯.choose, ⋯⟩) t
⊢ (fun i ↦ ↑(ks i)) 0 = b

Tactic:
simp [ks]

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

Goal state before:
pp: case refine_2
α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ ⨆ p ∈ ↑P ×ˢ ↑Q, p.1 ⊓ p.2 ≤ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}

Tactic:
· exact iSup₂_le fun (p, q) ⟨hp, hq⟩ ↦ le_sSup_of_le ⟨p, hp, q, hq, rfl⟩ (by simp)

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous fun a ↦ f (a, b)
⊢ ScottContinuousOn univ f

Tactic:
exact .fromProd (fun a ↦ (h₁ a).scottContinuousOn) (fun b ↦ (h₂ b).scottContinuousOn)
    (fun a ↦ (h₁ a).monotone) (fun b ↦ (h₂ b).monotone)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x))

Tactic:
exact (h i).comp_measurable measurable_prodMk_left

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:
rw [Pi.sub_apply] at hω

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
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω

Tactic:
upperCrossingTime_succ

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n ↦ upperCrossingTime a b f N n ω

Tactic:
exact monotone_nat_of_le_succ fun n =>
    le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ

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

Tactic:
have h_top : hittingAfter u s n ω ≠ ⊤ := fun h ↦ by simp [h] at h'
    have h_le := le_hittingAfter (u := u) (s := s) (n := n) ω
    refine ⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩
    lift (hittingAfter u s n ω) to ι using h_top with i'
    norm_cast at h' h_le

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

Tactic:
have hni : n < i := (le_hittingBtwn_of_exists h).trans_lt h'

Goal state after:
case mp
Ω : 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
hni : n < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ hittingBtwn f (Set.Iic a) 0 N ω = hittingBtwn f (Set.Iic a) 0 M ω

Tactic:
refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_

Goal state after:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
⊢ hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) N ω =
    hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) M ω

Tactic:
refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_

Goal state after:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω

Tactic:
refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
h_set_eq_Union : {ω | hittingAfter u s n ω ≤ ↑i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s
⊢ MeasurableSet {ω | hittingAfter u s n ω ≤ ↑i}

Tactic:
simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
    MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

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

Goal state before:
pp: case neg
Ω : 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)}
h𝓕_eq_iInf : ↑f t = ⨅ m_1, ↑f (s m_1)
k : ℕ
h_eq_k : ⋂ m, {ω | τ ω < ↑(s m)} = ⋂ m, ⋂ (_ : s m ≤ s k), {ω | τ ω < ↑(s m)}
⊢ MeasurableSet (⋂ m, {ω | τ ω < ↑(s m)})

Tactic:
rw [h_eq_k]

Goal state after:
case neg
Ω : 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)}
h𝓕_eq_iInf : ↑f t = ⨅ m_1, ↑f (s m_1)
k : ℕ
h_eq_k : ⋂ m, {ω | τ ω < ↑(s m)} = ⋂ m, ⋂ (_ : s m ≤ s k), {ω | τ ω < ↑(s m)}
⊢ MeasurableSet (⋂ m, ⋂ (_ : s m ≤ s k), {ω | τ ω < ↑(s m)})
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ 0 ≤ ∫ (x : Ω), stoppedValue f π x ∂μ - ∫ (x : Ω), stoppedValue f τ x ∂μ

Tactic:
← integral_sub',

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ 0 ≤ ∫ (a : Ω), (stoppedValue f π - stoppedValue f τ) a ∂μ

case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ Integrable (stoppedValue f π) μ

case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ Integrable (stoppedValue f τ) μ
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]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ∞
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
induction s, hs
    using MeasurableSpace.induction_on_inter (MeasurableSpace.measurableSpace_iSup_eq ℱ) hpi with

Goal state after: