mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ c,
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ n,
          ¬↑p ∣ n ∧
            ∃ gp,
              gp.natDegree ≤ p * f.natDegree - 1 ∧
                ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • cexp r - p • (aeval r) gp‖ ≤ c ^ p / ↑(p - 1)!

Tactic:
nsmul_eq_mul,

Goal state after:
f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ c,
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ n,
          ¬↑p ∣ n ∧
            ∃ gp,
              gp.natDegree ≤ p * f.natDegree - 1 ∧
                ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • cexp r - ↑p * (aeval r) gp‖ ≤ c ^ p / ↑(p - 1)!
Module: Mathlib.NumberTheory.RamificationInertia.Basic

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

Tactic:
IsDedekindDomain.ramificationIdx'_eq_factors_count hp (Factors.isPrime p P)
            (Factors.ne_bot p P)

Goal state after:
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)
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.Topology.Instances.Irrational

Goal state before:
pp: a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ (Ioo ↑a ↑b ∩ {x | Irrational x}).Nonempty

Tactic:
inter_comm

Goal state after:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ ({x | Irrational x} ∩ Ioo ↑a ↑b).Nonempty
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

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

Tactic:
inter_comm

Goal state after:
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}
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x + ↑(-⌊x⌋) ∈ Ico 0 1

Tactic:
simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff,
        mem_Ico, Int.cast_neg, le_add_neg_iff_add_le]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

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

Tactic:
by
        simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]

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}
⊢ a⁻¹ * b ∈ {b | orderOf b = n}

pp: case refine_2
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}
⊢ f ⟨a⁻¹ * b, ?refine_1⟩ = ⟨b, hb⟩

Tactic:
· rw [mem_ofPred_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]
      apply han
      simpa

Goal state after:
case refine_2
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}
⊢ f ⟨a⁻¹ * b, ⋯⟩ = ⟨b, hb⟩
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
x : α
hx : x ∈ c'.extent
hx' : x ∈ c'.intent
⊢ False

Tactic:
exact irrefl x (rel_extent_intent hx hx')

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ c'.intent

Tactic:
rw [← upperPolar_extent]
  exact fun z hz ↦ _root_.trans (rel_extent_intent hz hx) hy

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ c < principal a ↔ ∃ b ∈ c.right, b < a

Tactic:
by
  rw [← not_le, principal_le_iff]
  rw [not_iff_comm, not_exists, ← principal_le_iff]
  rw [← intent_subset_intent_iff]
  simp_rw [← not_le, not_and, not_not]
  rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ {x} ⊆ s

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
⊢ ⋃ a, B ⋯ ⊆ s

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_2.inl.inr
α : 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'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

pp: case refine_2.inr.inl
α : 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'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

pp: case refine_2.inr.inr
α : 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'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
· exact (h.2 (_root_.trans ya (_root_.trans ab bx))).elim

Goal state after:
case refine_2.inr.inl
α : 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'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

case refine_2.inr.inr
α : 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'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_2
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ tᶜ ∈ l

Tactic:
rw [← compl_subset_compl] at hsub

Goal state after:
case refine_2
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Tactic:
← l₂.mem_sets

Goal state after:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
unfold RTendsto' rcomap'

Goal state after:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
p : α → Prop
⊢ (∃ᶠ (x : α) in cocardinal α hreg, p x) ↔ c ≤ #↑{x | p x}

Tactic:
simp only [Filter.Frequently, eventually_cocardinal, not_not, coe_ofPred, not_lt]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • (T / ↑(n + 1)))

Tactic:
nsmul_eq_mul,

Goal state after:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (↑(n + 1) * (T / ↑(n + 1)))
Module: Mathlib.Order.Monotone.MonovaryOrder

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

pp: case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s

Tactic:
· 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

Goal state after:
case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ y hy

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)

Tactic:
refine StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
· rw [MeasurableSpace.map_def,
      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
    · simp
    · ext p
      simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
        Set.mem_empty_iff_false, iff_false, not_and]
      exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
ω : Ω
hω : predictablePart f ℱ μ n ω = 0 ω
⊢ martingalePart f ℱ μ n ω = f n ω

Tactic:
simp [martingalePart, hω]

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

Goal state before:
pp: case refine_1
Ω : 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 x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ MeasurableSet (⋃ n, {n} ×ˢ (Function.curry (Y m) n ⁻¹' {s}))

Tactic:
refine MeasurableSet.iUnion <| fun n ↦ ?_

Goal state after:
case refine_1
Ω : 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 x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
⊢ MeasurableSet ({n} ×ˢ (Function.curry (Y m) n ⁻¹' {s}))
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : 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 x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ { toFun := Y m, measurableSet_fiber' := ⋯, finite_range' := ⋯ } (n, ω) = X m (n, ω)

Tactic:
by simp; grind

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
⊢ MeasurableSet (⋃ (_ : j < ↑i), {ω | τ ω ≤ j})

Tactic:
rw [Set.iUnion_eq_if]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
⊢ MeasurableSet (if j < ↑i then {ω | τ ω ≤ j} else ∅)
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 : ι
hnm : n ≤ m
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
exact hnm

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < ↑i
⊢ ∃ i, k ≤ ↑(seq i)

Tactic:
rw [tendsto_atTop'] at h_tendsto
      cases k with
      | top => simp at hk_lt_i
      | coe k =>
        norm_cast at hk_lt_i ⊢
        have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
        obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
        exact ⟨a, ha a le_rfl⟩

Goal state after:
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 ω) ≤ upcrossingsBefore a b f N ω • (b - a)

Tactic:
nsmul_eq_mul,

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.Martingale.Upcrossing

Goal state before:
pp: case refine_2
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺

Tactic:
← sub_le_sub_iff_right a

Goal state after:
case refine_2
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ f ω i - a
⊢ b - a ≤ (f ω i - a)⁺
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos.hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (fun ω ↦ ↑(upcrossingsBefore a b f n ω)) μ

Tactic:
exact fun n => measurable_from_top.comp_aemeasurable
        (hf.stronglyAdapted.measurable_upcrossingsBefore hab).aemeasurable

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
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 huv _ hueq

Goal state after:
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 < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i} = (stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i}
⊢ MeasurableSet ((stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i})

Tactic:
exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
m : ι
hm : m ∈ {i ∈ s | i < n}
⊢ ω ∉ {ω | τ ω = ↑m}

Tactic:
rw [Finset.mem_filter] at hm

Goal state after:
case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ω ∉ {ω | τ ω = ↑m}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Tactic:
rw [sum_insert hi_notin_s]

Goal state after:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * (X i + ∑ x ∈ s, X x) ω)) μ