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

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ ‖↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p

Tactic:
← h',

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ ‖↑(eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p))) * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : 0 < b ∧ b < p
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

Tactic:
pos_iff_ne_zero

Goal state after:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, ↑a = ↑(↑a).val

Tactic:
rintro a -

Goal state after:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
⊢ ↑a = ↑(↑a).val
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b

Tactic:
rw [sub_div' hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_iff_of_pos_right hb0, abs_sub_lt_iff,
    sub_lt_iff_lt_add, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: n : ℕ
h : n ≠ 1
⊢ Prime n ↔ ↑(n - 1)! = -1

Tactic:
refine ⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
  have := Fact.mk h1
  exact ZMod.wilsons_lemma n

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

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

Tactic:
mul_div_mul_right _ _ (by positivity)

Goal state after:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑m / ↑n + ↑r.num / ↑r.den = ↑m / ↑n + ↑r.num / ↑r.den
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)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ∞

Tactic:
have : ∀ b : ℕ, volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤
      ↑(2 * ((b : ℝ≥0) ^ (1 - r) + (b : ℝ≥0) ^ (-r))) := fun b ↦
    calc
      volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ∑ a ∈ Finset.Icc (0 : ℤ) b, volume (B a b) :=
        measure_biUnion_finset_le _ _
      _ = ↑((b + 1) * (2 / (b : ℝ≥0) ^ r)) := by
        simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero,
          Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]
      _ = _ := by
        have : 1 - r ≠ 0 := by linarith
        rw [ENNReal.coe_inj]
        simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
          mul_left_comm]

Goal state after:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ∞
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) → ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

pp: case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
· rintro ⟨y, ⟨m, hm₁, hm₂, rfl⟩, hx⟩; exact ⟨m, hm₁, hm₂, hx⟩

Goal state after:
case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter β
inst✝ : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (comap f l) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter β
inst✝ : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ comap f l
⊢ ⋂₀ S ∈ comap f l
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter α
inst✝ : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (map f l) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter α
inst✝ : CardinalInterFilter l c
f : α → β
S : Set (Set β)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ map f l
⊢ ⋂₀ S ∈ map f l
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
⊢ CardinalInterFilter (l₁ ⊓ l₂) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩

Goal state after:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: case mp
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
      exact ⟨v, vsets, (SetRel.preimage_mono hv).trans h⟩

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ μ univ ≤ ∑ x, μ (closedBall (↑x • ξ) (δ / 2))

Tactic:
μ.addHaar_closedBall_center,

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ μ univ ≤ ∑ x, μ (closedBall 0 (δ / 2))
Module: Mathlib.Order.Monotone.MonovaryOrder

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

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_monotoneOn]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ⊆ R.leftDual J

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Goal state after:
case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ J ⊆ R.rightDual (R.leftDual J)
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ (fun b ↦ ∀ ⦃a : α⦄, a ∈ J → (a, b) ∈ R) ≤ fun b ↦ ∀ ⦃a : α⦄, a ∈ J' → (a, b) ∈ R

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ J ⊆ J'
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.leftDual (R.rightDual I) ⊆ R.leftDual (R.rightDual I')

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.rightDual I' ⊆ R.rightDual I
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 β
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
by
  rw [iSup₂_le_iff]; intro y hy
  rw [le_iInf₂_iff]; intro x hx
  exact iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))

Goal state after:
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 ≤ f a b

Tactic:
rw [← h]
      apply le_iSup₂ y hy

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

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂

Tactic:
rw [SubRootedTree.mem_iff] at h₁ h₂
    contrapose h
    rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h
    rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh
    · simp_all [RootedTree.subtrees, IsAtom.lt_iff]
    rw [le_inf_iff] at oh
    ext
    simpa only [ht₂.le_iff_eq ht₁.1, ht₁.le_iff_eq ht₂.1, eq_comm, or_self] using
      le_total_of_directed oh.2 h₂

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range ⇑n
b : X
h1 : b ∈ a
⊢ n (sInf a) ≤ b

Tactic:
subset_def,

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
h : ∀ x ∈ a, x ∈ range ⇑n
b : X
h1 : b ∈ a
⊢ n (sInf a) ≤ b
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 g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : predictablePart (f + g) ℱ μ n ω = predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω
⊢ f n ω + g n ω - (predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω) =
    f n ω - predictablePart f ℱ μ n ω + (g n ω - predictablePart g ℱ μ n ω)

Tactic:
abel

Goal state after:
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✝ : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
⊢ Supermartingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
  filter_upwards [condExp_ae_le hf hij, condExp_congr_ae (h_eq j), h_eq i] with ω h_le hcond h_eq
  rwa [← hcond, ← h_eq]

Goal state after:
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 : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Supermartingale (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 (condExp_add (hf.integrable j) (hg.integrable j) _).le.trans ?_
  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.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

Tactic:
· exact (hittingBtwn_eq_hittingBtwn_of_exists hm h).le

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
⊢ Monotone (hittingAfter u s)

Tactic:
by
  intro n m hnm ω
  simp only [hittingAfter]
  split_ifs with h_n h_m h_m
  · norm_cast
    gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]
  · simp
  · have ⟨t, ht⟩ := h_m
    exact absurd ⟨t, hnm.trans ht.1, ht.2⟩ h_n
  · simp

Goal state after:
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:
rw [← sub_le_sub_iff_right a] at h
      rwa [posPart_eq_self.2 (le_trans hab'.le h)]

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

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | ↑i ≤ ↑i_1})
h' : MeasurableSet (s ∩ {ω | ↑i ≤ ↑i})
⊢ MeasurableSet s

Tactic:
simpa only [le_refl, Set.ofPred_true, Set.inter_univ] using h'

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
⊢ ↑ε ≤ f m ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

Tactic:
hεm

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : ↑ε ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
· lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht
      norm_cast
      refine hx_fst_le.trans (le_of_lt ?_)
      convert! ω.prop
      simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_ofPred_eq, ← ht]
      norm_cast

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
ω : Ω
h : π ω = ⊤
⊢ False

Tactic:
specialize hbdd ω; simp [h] at hbdd

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp ((0 + t) * X ω)) μ

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp ((0 - t) * X ω)) μ

Tactic:
· simpa using ht_int_pos

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp ((0 - t) * X ω)) μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ complexMGF id (Measure.map X μ) = complexMGF X μ

Tactic:
by
  ext t
  rw [complexMGF, integral_map hX]
  · rfl
  · fun_prop

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

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
| succ n hn =>

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
induction n generalizing t with
  | zero => simp [hasDerivAt_mgf ht]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (mgf X μ))
        =ᶠ[𝓝 t] fun t ↦ μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp_real ht (n + 1)

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

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
| succ n hn =>

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ rexp ((0 + t) * X ω)) μ

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ rexp ((0 - t) * X ω)) μ

Tactic:
· simpa using ht_int_pos

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ rexp ((0 - t) * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + (u - v) = u

Tactic:
abel

Goal state after: