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
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}

Tactic:
let σL := WithVal.valueGroupOrderIso₀ (w.valuation L)

Goal state after:
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
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: 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
w : K⟮X⟯
h0 : w ≠ 0
h1 : v w < 1
⊢ {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty

Tactic:
induction w using RatFunc.induction_on with
  | f p q =>
    simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *
    have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; aesop
    suffices ∀ r : K[X], v (↑r) ≠ 1 → r ≠ 0 → {p : K[X] | v ↑p < 1 ∧ ¬p = 0}.Nonempty by
      exact Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)
    exact fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr
      ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩

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

Goal state before:
pp: case hH.refine_1
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ k, ⋯.unit ^ k = γ
k : ℤ
hk : ⋯.unit ^ k = γ
⊢ ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x

Tactic:
use 1, one_ne_zero, πᵥ ^ k
      simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val] at hk
      simp [← hk]

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

Goal state before:
pp: x : ℤ[i]
⊢ { re := ↑(star x).re, im := ↑(star x).im } = (starRingEnd ℂ) (toComplex x)

Tactic:
toComplex_def₂

Goal state after:
x : ℤ[i]
⊢ { re := ↑(star x).re, im := ↑(star x).im } = (starRingEnd ℂ) { re := ↑x.re, im := ↑x.im }
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ n = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
by rw [h₁, h]; ring

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

Goal state before:
pp: f : ℂ[X]
s : ℂ
⊢ P f s = cexp s * eval 0 (sumIDeriv f) - eval s (sumIDeriv f)

Tactic:
P

Goal state after:
f : ℂ[X]
s : ℂ
⊢ cexp s * eval 0 (sumIDeriv f) - eval s (sumIDeriv f) = cexp s * eval 0 (sumIDeriv f) - eval s (sumIDeriv f)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, (↑a).val ∈ Ico 1 (p - 1).succ

Tactic:
intro a ha

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ∈ Ico 1 (p - 1).succ
Module: Mathlib.Order.CompleteSublattice

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

Tactic:
iInf,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ↑(sInf (range f)) = ⨅ i, ↑(f i)
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (⨅ i, f i).extent = ⋂ i, (f i).extent

Tactic:
iInf,

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (sInf (range fun i ↦ f i)).extent = ⋂ i, (f i).extent
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (⨅ i, f i).intent = upperPolar r (⋂ i, (f i).extent)

Tactic:
iInf,

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (sInf (range fun i ↦ f i)).intent = upperPolar r (⋂ i, (f i).extent)
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_2
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a} ⊆ countableSupClosure s

Tactic:
rintro _ ⟨u, hus, rfl⟩

Goal state after:
case refine_2
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
u : ℕ → α
hus : ∀ (n : ℕ), u n ∈ s
⊢ ⨆ n, u n ∈ countableSupClosure s
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ l : Filter α
inst✝ : CountableInterFilter l
S : Set (Set α)
hS : #↑S < ℵ_ 1
a : ∀ s ∈ S, s ∈ l
⊢ ⋂₀ S ∈ l

Tactic:
apply CountableInterFilter.countable_sInter_mem S _ a
    rwa [← le_aleph0_iff_set_countable, ← lt_aleph_one_iff]

Goal state after:
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 α
⊢ (∃ a, (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) → ∃ a ∈ l, r.core (s.core a) ⊆ t

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

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

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁

Tactic:
intro h'

Goal state after:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
⊢ ∀ s ∈ l₂, f.preimage s ∈ l₁
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case neg
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∃ p, ¬A ↑p =ᵐ[μ] ∅ ∨ ¬B ↑p =ᵐ[μ] ∅
⊢ E =ᵐ[volume] ∅ ∨ E =ᵐ[volume] univ

Tactic:
· right
    obtain ⟨p, hp⟩ := h
    rw [hE₁ p]
    cases hp
    · rcases hA p with _ | h; · contradiction
      simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left]
    · rcases hB p with _ | h; · contradiction
      simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left,
        union_ae_eq_univ_of_ae_eq_univ_right]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ (iInf f) x = ⨅ j, (f j) x

Tactic:
iInf,

Goal state after:
X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ (sInf (range f)) x = ⨅ j, (f j) x
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = s

Tactic:
simp_rw [← P.sSup_eq, sSup_eq_iSup]
  rfl

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m

Tactic:
rw [hittingBtwn, ite_eq_right_iff]

Goal state after:
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 : ℕ
⊢ predictablePart (f + g) ℱ μ n =ᵐ[μ] g n

Tactic:
filter_upwards [martingalePart_add_ae_eq hf hg hg0 hgint n] with ω hω

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ω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ predictablePart (f + g) ℱ μ n ω = g n ω
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 : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
· exact hittingBtwn_mem_set h

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i → ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
intro h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : hittingBtwn u s n m ω ≤ i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingBtwn u s n m ω ≤ i

Tactic:
intro h'

Goal state after:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

Tactic:
rw [not_lt] at hN'
    exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N k ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N k ω)
n : ℕ
⊢ MeasurableSet {ω | ↑(hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω) ≤ ↑n}

Tactic:
refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N k ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N k ω)
n : ℕ
⊢ ∀ (x : Ω), ↑(lowerCrossingTime a b f N k x) ≤ ↑N
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
⊢ hittingAfter u s n ω ≤ ↑i → ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
intro h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ ↑i
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
⊢ (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingAfter u s n ω ≤ ↑i

Tactic:
intro h'

Goal state after:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
⊢ hittingBtwn u s n m ω < i → ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
intro h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
⊢ (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingBtwn u s n m ω < i

Tactic:
intro h'

Goal state after:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω < i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
⊢ hittingAfter u s n ω < ↑i → ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
intro h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
⊢ (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingAfter u s n ω < ↑i

Tactic:
intro h'

Goal state after:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingAfter u s n ω < ↑i
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✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω < ↑i}ᶜ

Tactic:
exact (hτ.measurableSet_lt i).compl

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
a : ι
⊢ ↑a ≤ ↑i ↔ ∃ i_1 ≤ i, ↑a = ↑i_1

Tactic:
norm_cast; simp

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

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

Tactic:
intro n n' hnn' ω
  simp only [hittingBtwn]
  split_ifs with h_n h_n' h_n'
  · gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]
  · obtain ⟨t, ht⟩ := h_n
    exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2
  · have ⟨t, ht⟩ := h_n'
    exact absurd ⟨t, ⟨hnn'.trans ht.1.1, ht.1.2⟩, ht.2⟩ h_n
  · simp

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : DenselyOrdered ι
inst✝³ : FirstCountableTopology ι
inst✝² : NoMaxOrder ι
κ : Type u_4
inst✝¹ : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst✝ : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
⊢ IsStoppingTime f fun ω ↦ ⨅ n, τ n ω

Tactic:
convert! IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n) using 2

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : DenselyOrdered ι
inst✝³ : FirstCountableTopology ι
inst✝² : NoMaxOrder ι
κ : Type u_4
inst✝¹ : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst✝ : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
x✝ : Ω
⊢ ⨅ n, τ n x✝ = ⨅ n ∈ Set.univ, τ n x✝
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
refine ⟨hs.1.compl, fun i ↦ ?_⟩

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ MeasurableSet (sᶜ ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ MeasurableSet (sᶜ ∪ {ω | τ ω ≤ ↑i}ᶜ)

Tactic:
rw [← Set.compl_inter]
        exact (hs.2 i).compl

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
n : ℕ
ω : Ω
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖

Tactic:
by_cases! hnonneg : 0 ≤ f n ω - a
        · rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
        · rw [posPart_eq_zero.2 hnonneg.le]
          exact norm_nonneg _

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[μ.trim hle] g
ω : Ω
hω : g' ω = g ω
hg'ω : Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
⊢ Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
exact hω ▸ hg'ω

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
nth_rewrite 2 [untopA_eq_untop]

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑((min (↑i) (σ ω)).untop ?neg✝)) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i) (σ ω) ≠ ⊤