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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : K
⊢ (valuation K v) x ^ v.asIdeal.ramificationIdx' w.asIdeal = (valuation L w) ((algebraMap K L) x)

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) x
  simp [valuation_of_algebraMap, div_pow, ← IsScalarTower.algebraMap_apply A K L,
    IsScalarTower.algebraMap_apply A B L, intValuation_liesOver v w]

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

Goal state before:
pp: case inr
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1

Tactic:
induction f using RatFunc.induction_on with
    | f p q hq0 =>
      have hp0 : p ≠ 0 := by simp_all
      set pi := πᵥ with hpi_def
      have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer hle
      simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0,
        if_neg hq0, div_inv_eq_mul]
      rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]
      simp_all [div_le_one₀, inv_mul_le_one₀,
        (pow_le_pow_iff_right_of_lt_one₀ (by simp_all) (IsRankOneDiscrete.generator_lt_one v))]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ { re := ↑k, im := 1 } * { re := ↑k, im := -1 } = ↑p * ↑y

Tactic:
rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
P_eq_integral_exp_mul_eval (f p) s,

Goal state after:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p))‖ ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case hbc
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in Set.Ioc 0 1, cexp (-(x • s)) * eval (x • s) (f p) ∂MeasureTheory.volume‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
← mul_one (_ * _)

Goal state after:
case hbc
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in Set.Ioc 0 1, cexp (-(x • s)) * eval (x • s) (f p) ∂MeasureTheory.volume‖ ≤ Real.exp ‖s‖ * |c| ^ p * 1
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval α fR - eval (↑z / (↑a + 1)) fR|

Tactic:
rw [fa, zero_sub, abs_neg]

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0

Tactic:
simp only [← ofPred_exists, exists_prop]

Goal state after:
⊢ volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m ↦ 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|

Tactic:
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m ↦ 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ), (∀ (m : ℤ), 1 / ↑b ^ x_1 ≤ dist x (↑m / ↑b)) → ∀ (a : ℤ), 1 / ↑b ^ x_1 ≤ |x - ↑a / ↑b|
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
⊢ sInf s i = ⨅ e, ↑e i

Tactic:
by
  simp [sInf, inf]

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Codisjoint a b ↔ Codisjoint ↑a ↑b

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ Codisjoint ↑a ↑b
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ Codisjoint ↑a ↑b

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ ↑a ⊔ ↑b = ⊤
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_1.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 c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

pp: case refine_1.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 c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
· exact Or.inr ⟨ax, _root_.trans yb bc⟩

Goal state after:
case refine_1.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 c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : x < f 0
i : Fin n
⊢ insertNth 0 x f i.succ.castSucc < insertNth 0 x f i.succ.succ

Tactic:
· simpa using hf i

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ Filter α

Tactic:
apply ofCardinalUnion {s | Cardinal.mk s < c} (natCast_lt_aleph0.trans_le hreg.aleph0_le)
  · refine fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_
    apply iSup_lt_of_lt_cof_ord _ fun i ↦ hSc i.1 i.2
    rwa [hreg.cof_ord]
  · exact fun _ hSc _ ht ↦ lt_of_le_of_lt (mk_le_mk_of_subset ht) hSc

Goal state after:
Module: Mathlib.Order.KonigLemma

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

Tactic:
by simp [ks]

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

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
⊢ ∃! y, y ∈ Q ∧ x ≤ y

Tactic:
by
  obtain ⟨y, hy, hxy⟩ := h hx
  refine ⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ ↦ Q.eq_of_not_disjoint hz hy ?_⟩
  have := P.ne_bot_of_mem hx
  contrapose this
  exact le_bot_iff.mp (this hxz hxy)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x✝¹ : Set α
d₁ : x✝¹.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝¹
x✝ : α
hda : IsLUB x✝¹ x✝
⊢ IsLUB (f '' x✝¹) (f x✝)

Tactic:
by rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]

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
a b : X
s : ↥S
⊢ a ≤ ↑(Sublocale.restrictAux✝ S b ⇨ s) ↔ ↑(Sublocale.restrictAux✝ S b) ≤ a ⇨ ↑s

Tactic:
@le_himp_comm,

Goal state after:
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
a b : X
s : ↥S
⊢ a ≤ ↑(Sublocale.restrictAux✝ S b ⇨ s) ↔ a ≤ ↑(Sublocale.restrictAux✝ S b) ⇨ ↑s
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
⊢ t.subtrees.PairwiseDisjoint SetLike.coe

Tactic:
intro t₁ ht₁ t₂ ht₂ h
  rw [Function.onFun_apply, Set.disjoint_left]
  intro a ha hb
  rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h
  subst h
  simp only [SetLike.mem_coe, SubRootedTree.bot_mem_iff] at ha
  exact t₁.root_ne_bot_of_mem_subtrees ht₁ ha

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: ⊢ card 1 = 1

Tactic:
simpa using card_type (α := PUnit)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
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)

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:
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m)) (n + 1)
m : ℕ
⊢ (Set.range (X m)).Finite

Tactic:
apply (h𝓕.approx m).finite_range.subset

Goal state after:
case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := ⋯
this : MeasurableSpace Ω := ⋯
X : ℕ → Ω → E := ⋯
m : ℕ
⊢ Set.range (X m) ⊆ Set.range ⇑(StronglyMeasurable.approx h𝓕 m)
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: case refine_1
Ω : 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
⊢ μ[f 0 | ↑ℱ i] =ᵐ[μ] f 0

Tactic:
rw [condExp_of_stronglyMeasurable (ℱ.le _) _ (hf_int 0)]

Goal state after:
Ω : 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
⊢ StronglyMeasurable (f 0)
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 : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
k : ℕ
hk : i ≤ k
this : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ i]
x : Ω
hx : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] x = μ[f (k + 1) - f k | ↑ℱ i] x
⊢ μ[f (k + 1) - f k | ↑ℱ i] x - μ[f (k + 1) - f k | ↑ℱ i] x = 0

Tactic:
sub_self

Goal state after:
Ω : 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
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
k : ℕ
hk : i ≤ k
this : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ i]
x : Ω
hx : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] x = μ[f (k + 1) - f k | ↑ℱ i] x
⊢ 0 = 0
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
x✝ : (μ.trim ⋯) s < ∞
⊢ 0 ≤ ∫ (x : Ω) in s, (μ[f j | ↑ℱ i] - f i) x ∂μ.trim ⋯

Tactic:
specialize hf i j hij s hs

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
i j : ι
hij : i ≤ j
s : Set Ω
hf : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
hs : MeasurableSet s
x✝ : (μ.trim ⋯) s < ∞
⊢ 0 ≤ ∫ (x : Ω) in s, (μ[f j | ↑ℱ i] - f i) x ∂μ.trim ⋯
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ f + g = martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ

Tactic:
martingalePart_add_predictablePart

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ f + g = f + g
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ hittingAfter u Set.univ n ω = ↑n

Tactic:
simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f (i + 1) - f i | ↑𝒢 i]
i : ℕ
⊢ f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]

Tactic:
← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _),

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f (i + 1) - f i | ↑𝒢 i]
i : ℕ
⊢ μ[f i | ↑𝒢 i] ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]

Tactic:
← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _),

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0
i : ℕ
⊢ μ[f i | ↑𝒢 i] =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j, n ≤ j ∧ u j ω ∈ F
hE : ∃ j, n ≤ j ∧ u j ω ∈ E
⊢ n ∈ lowerBounds {j | n ≤ j ∧ u j ω ∈ F}

Tactic:
by simp only [mem_lowerBounds]; grind

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (n + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N n ω)) ω =
    0

Tactic:
have : N ≤ upperCrossingTime a b f N n ω := by
    rw [upcrossingsBefore] at hn
    rw [← not_lt]
    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
  simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
    lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]

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

Goal state before:
pp: case pos
Ω : 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 ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f (↑N).untopA ω - f (↑N).untopA ω

Tactic:
sub_self

Goal state after:
case pos
Ω : 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 ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ 0
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
m : ι
hm : n < m
t : ι
hτ : ↑t = ↑m
hτbdd : ↑t ≤ ↑N
⊢ m ≤ N

Tactic:
hτ

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
m : ι
hm : n < m
t : ι
hτ : ↑t = ↑m
hτbdd : ↑m ≤ ↑N
⊢ m ≤ N