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

Goal state before:
pp: case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
· rintro ⟨a, b, h₁, h₂⟩
    obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂
    exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩

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

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

Tactic:
obtain fR0 : fR ≠ 0 := fun fR0 =>
    (map_injective (algebraMap ℤ ℝ) fun _ _ A => Int.cast_inj.mp A).ne f0
      (fR0.trans (Polynomial.map_zero _).symm)

Goal state after:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
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:
specialize h a b.pred

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
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
h : 1 ≤ (↑b.pred + 1) ^ f.natDegree * (|x - ↑a / (↑b.pred + 1)| * A)
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.Residual

Goal state before:
pp: ⊢ {x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
refine Subset.antisymm ?_ ?_

Goal state after:
case refine_1
⊢ {x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

case refine_2
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}
Module: Mathlib.Order.Bounded

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

Tactic:
convert! @unbounded_le_inter_not_le _ s _ a
  exact lt_iff_not_ge

Goal state after:
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:
exact bounded_lt_inter_lt a

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ↑(iInf f) = ⨅ i, ↑(f i)

Tactic:
rw [iInf, coe_sInf', iInf_range]

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ principal a ≤ c ↔ a ∈ c.left

Tactic:
by
  simp only [← extent_subset_extent_iff, left_principal]
  exact ⟨fun h ↦ h self_mem_Iic, fun h y hy ↦ mem_extent_of_rel_extent hy h⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
x : α
s : Set α
hs_subset : s ⊆ {x}
hs_ne : s.Nonempty
x✝ : s.Countable
y : α
hy : IsLUB s y
⊢ s = {x}

Tactic:
ext y

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
x : α
s : Set α
hs_subset : s ⊆ {x}
hs_ne : s.Nonempty
x✝ : s.Countable
y✝ : α
hy : IsLUB s y✝
y : α
⊢ y ∈ s ↔ y ∈ {x}
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂

Tactic:
rw [← tendsto_iff_ptendsto]
  simp [principal_univ]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑sᶜ < ℵ_ 1 ↔ #↑sᶜ ≤ ℵ₀

Tactic:
lt_aleph_one_iff

Goal state after:
α : Type u
s : Set α
⊢ #↑sᶜ ≤ ℵ₀ ↔ #↑sᶜ ≤ ℵ₀
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ MonotoneOn g s

Tactic:
classical
  let := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
        ⟨J, hJ⟩) =
    ⟨J, hJ⟩

Tactic:
Subtype.mk.injEq,

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
⊢ R.rightDual (R.leftDual J) = J
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
        ⟨I, hI⟩) =
    ⟨I, hI⟩

Tactic:
Subtype.mk.injEq,

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ R.leftDual (R.rightDual I) = I
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x

Tactic:
ext y

Goal state after:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
y : α
⊢ y ∈ t ↔ y ∈ P.partOf x
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ P.Rel x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf x = P.partOf y

Tactic:
by
  grind [rel_iff_partOf_eq_partOf_of_mem, Rel.left_mem, Rel.right_mem]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ sInf {s_1 | sSup s ≤ ↑s_1} = sSup ((fun x ↦ sInf {s | x ≤ ↑s}) '' s)

Tactic:
by
    change Sublocale.restrictAux S (sSup s) = _
    rw [S.giAux.gc.l_sSup, sSup_image]
    rfl

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

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1 | ↑ℱ i_1] | ↑ℱ i] =ᵐ[μ]
    ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])

Tactic:
exact eventuallyEq_sum fun k _ => condExp_sub (by fun_prop) integrable_condExp _

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:
rw [Set.mem_inter_iff] at hb
      exact hb.1.1

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (↑(lowerCrossingTime a b f N n ω)).untopA ω ≤ a

Tactic:
exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)

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

Goal state before:
pp: case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : j < i
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)

Tactic:
· rw [min_eq_right (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_left (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
    refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
by
  have h₁ : (0 : ℝ) ≤
      μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] := by
    have := (hf.sum_sub_upcrossingStrat_mul a b N).setIntegral_le (zero_le (a := n)) .univ
    rw [setIntegral_univ, setIntegral_univ] at this
    refine le_trans ?_ this
    simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]
  have h₂ : μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] =
    μ[∑ k ∈ Finset.range n, (f (k + 1) - f k)] -
      μ[∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)] := by
    simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply,
      Pi.mul_apply]
    refine integral_sub (Integrable.sub (integrable_finsetSum _ fun i _ => hf.integrable _)
      (integrable_finsetSum _ fun i _ => hf.integrable _)) ?_
    convert! (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
    ext; simp
  rw [h₂, sub_nonneg] at h₁
  refine le_trans h₁ ?_
  simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f ⊥ ω = ⊥

Tactic:
simp [upcrossingsBefore]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0

Tactic:
simp [upcrossingsBefore]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
⊢ Antitone fun x ↦ hittingBtwn u x n m

Tactic:
intro E

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E : Set β
⊢ ∀ ⦃b : Set β⦄, E ⊆ b → (fun x ↦ hittingBtwn u x n m) b ≤ (fun x ↦ hittingBtwn u x n m) E
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : 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 = ⊥
h_eq : {ω | τ ω ≤ ↑t} = {ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t}
⊢ MeasurableSet ({ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t})

Tactic:
exact (hτ1 t).union (hτ2 t ht)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
⊢ Antitone fun x ↦ hittingAfter u x n

Tactic:
intro E

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E : Set β
⊢ ∀ ⦃b : Set β⦄, E ⊆ b → (fun x ↦ hittingAfter u x n) b ≤ (fun x ↦ hittingAfter u x n) E
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
h₂ :
  ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)

Tactic:
Finset.card_range,

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
h₂ :
  ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ upcrossingsBefore a b f N ω • (b - a)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω | π ω ≤ ↑i})

Tactic:
(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i})

Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ s ∩ {ω | π ω ≤ ↑i} = s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i}
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
ae_iff,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ (μ.trim ⋯) {a | ¬∃ c, Tendsto (fun n ↦ f n a) atTop (𝓝 c)} = 0
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ

Tactic:
intro σ π hσ hπ hσ_le_π hπ_bdd
    simp_rw [stoppedValue_stoppedProcess]
    obtain ⟨n, hπ_le_n⟩ := hπ_bdd
    have hπ_top ω : π ω ≠ ⊤ := ne_top_of_le_ne_top (by simp) (hπ_le_n ω)
    have hσ_top ω : σ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (hσ_le_π ω)
    simp only [ne_eq, hσ_top, not_false_eq_true, ↓reduceIte, hπ_top, ge_iff_le]
    exact h.expected_stoppedValue_mono (hσ.min hτ) (hπ.min hτ)
      (fun ω => min_le_min (hσ_le_π ω) le_rfl) fun ω => (min_le_left _ _).trans (hπ_le_n ω)

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
⊢ (∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) → stoppedAbove f r i ω ≤ r + ↑R

Tactic:
hbddω

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ stoppedAbove f r i ω ≤ r + ↑R
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case neg.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ ↑k < leastGE f r ω

Tactic:
suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
    have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
      ne_top_of_le_ne_top (by simp) (min_le_left _ _)
    lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p
    simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *
    lia

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ stoppedValue u τ = ∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)

Tactic:
ext y

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)) y
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x ↦ rexp (t * x)
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x ↦ rexp (t * x)
h'X : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ upperBounds (Set.range fun n ↦ (-f) n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -c ≤ ω

Tactic:
rw [mem_upperBounds] at hc

Goal state after:
case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n ↦ (-f) n ω✝, x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -c ≤ ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u (↑i).untopA ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

Tactic:
Finset.sum_eq_single_of_mem i

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u (↑i).untopA ω = {a | ↑n ≤ τ a}.indicator (u n) ω + {ω | τ ω = ↑i}.indicator (u i) ω

case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ {i ∈ s | i < n}

case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ∀ b ∈ {i ∈ s | i < n}, b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
⊢ stoppedProcess u τ n = {a | ↑n ≤ τ a}.indicator (u n) + ∑ i < n, {ω | τ ω = ↑i}.indicator (u i)

Tactic:
have h_mem : ∀ ω, τ ω < n → τ ω ∈ WithTop.some '' (Finset.Iio n) := by
    intro ω h
    simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]
    have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
    lift τ ω to ι using h_top with i hi
    exact ⟨i, mod_cast h, rfl⟩

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑(Finset.Iio n)
⊢ stoppedProcess u τ n = {a | ↑n ≤ τ a}.indicator (u n) + ∑ i < n, {ω | τ ω = ↑i}.indicator (u i)