mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
mul_sub

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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p

Tactic:
rw [← mul_pow, abs_of_nonneg (by positivity), max_def]

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p
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
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ 0 < finrank (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P)

Tactic:
rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]

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
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * p.inertiaDeg' ↑P ≠ 0
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))
⊢ ‖cexp r * ↑(eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p))) - (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:
← eq_intCast (algebraMap ℤ ℂ),

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))
⊢ ‖cexp r * (algebraMap ℤ ℂ) (eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p))) - (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.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x * ↑r - ↑m / ↑n * ↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p

Tactic:
← sub_mul,

Goal state after:
case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |(x - ↑m / ↑n) * ↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ ↑a₁✝ = ↑a₂✝

Tactic:
exact val_injective p h

Goal state after:
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ IsLUB (range u) c ↔ IsLUB (⋃ i, s i) c

Tactic:
refine isLUB_congr ?_

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ i, s i)
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y ∈ carrier

Tactic:
suffices x ⊔ y = sSup {x, y} by exact this ▸ sSupClosed' (fun z hz ↦ by aesop)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y = sSup {x, y}
Module: Mathlib.Order.Extension.Linear

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

Tactic:
refine ⟨s,
    { total := ?_, refl := hs.1.refl, trans := hs.1.trans, antisymm := hs.1.antisymm }, hrs⟩

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
⊢ ∀ (a b : α), s a b ∨ s b a
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x

Tactic:
simpa [Set.finite_singleton x] using hreg.nat_lt 1

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
⊢ ∀ i ≥ x ⊓ y, (⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y) ⊓ ⨅ y_1, ⨅ (_ : y_1 ≥ y), m y_1 ⇨ n y_1 ≤ m i ⇨ n i

Tactic:
have : Nonempty X := ⟨x⟩

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
⊢ ∀ i ≥ x ⊓ y, (⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y) ⊓ ⨅ y_1, ⨅ (_ : y_1 ≥ y), m y_1 ⇨ n y_1 ≤ m i ⇨ n i
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin✝ : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : (f i).fst = i
⊢ (f i).fst + 1 = i.succ

Tactic:
ih

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin✝ : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : (f i).fst = i
⊢ i + 1 = i.succ
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s t x✝ y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q P : Partition s
x : α
hxP : x ∈ P
⊢ ∃ y ∈ removeBot {s} ⋯ ⋯, x ≤ y

Tactic:
by simp [P.ne_bot_of_mem' hxP, P.le_of_mem hxP]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts
⊢ t ⊆ ⋃₀ S ↔ t ∈ S

Tactic:
rw [← subset_sUnion_and_mem_iff_mem hSP]
  simp [ht]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)

Tactic:
constructor
  · simp [hr]
  · intro b hb
    apply Order.le_pred_of_lt at hb
    simpa using hb

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)
⊢ MeasurableSet (⋂ m, {ω | τ ω < ↑(s m)})

Tactic:
h𝓕_eq_iInf

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)
⊢ MeasurableSet (⋂ m, {ω | τ ω < ↑(s m)})
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 ω)) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun j ↦ f (j + 1) ω - f j ω) x

Tactic:
simp_rw [h₁]

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 ω)) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (x + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N x ω)) ω)
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ≤ fun x ↦ ↑j

pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x ↦ ↑j) x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
· intro ω
    simp only [Set.piecewise, ENat.some_eq_natCast]
    split_ifs with hω
    · exact mod_cast hij
    · norm_cast

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x ↦ ↑j) x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
Module: Mathlib.Probability.Martingale.Convergence

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

Tactic:
← sub_ae_eq_zero,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ f n - μ[g | ↑ℱ n] =ᵐ[μ] 0
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ⨆ N, ↑(upcrossingsBefore a b f N ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
iSup_le_iff

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : 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)⁺ ∂μ)
⊢ ⨆ i, ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f i a_1) ∂μ ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
iSup_le_iff

Goal state after:
case pos
Ω : 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)⁺ ∂μ)
⊢ ∀ (i : ℕ),
    ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f i a_1) ∂μ ≤
      ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
rwa [Set.inter_assoc, Set.inter_self] at h'

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
⊢ MeasurableSet ({ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j})

Tactic:
refine MeasurableSet.inter ?_ (hτ.measurableSet_le j)

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
⊢ MeasurableSet {ω | min (τ ω) ↑j ≤ min (π ω) ↑j}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
⊢ Integrable X μ

Tactic:
have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable X μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:

Tactic:
a * t₁ + b * t₂
    _ ≤ a * t₂ + b * t₂ := by gcongr
    _ = t₂ := by rw [← add_mul, hab, one_mul]

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

Goal state before:
pp: case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [abs_of_nonpos ht_neg.le, sup_comm]

Goal state after:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
by
  rcases lt_or_gt_of_ne ht with ht_neg | ht_pos
  · rw [abs_of_nonpos ht_neg.le, sup_comm]
    convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])
    simp
  · rw [abs_of_nonneg ht_pos.le]
    exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ (√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v)) = (√(2 * π * ↑v))⁻¹ * rexp (-(x - (μ + y)) ^ 2 / (2 * ↑v))

Tactic:
sub_add_eq_sub_sub_swap

Goal state after:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ (√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v)) = (√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case hfi
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ Integrable (gaussianPDFReal μ v) (ℙ.restrict s)

pp: case f_nn
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᵐ[ℙ.restrict s] gaussianPDFReal μ v

Tactic:
· exact (integrable_gaussianPDFReal _ _).restrict

Goal state after:
case f_nn
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᵐ[ℙ.restrict s] gaussianPDFReal μ v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ MemLp X (↑p) μ

Tactic:
simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]
    exact hX.aestronglyMeasurable

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

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
· ext
    rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]
    rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
    contrapose h
    convert! (memLp_const (-c)).add h
    ext; simp

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [ENNReal.toReal_mul]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal