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

Goal state before:
pp: case refine_3
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ 𝓟D.ramificationIdxIn B ≤ P.ramificationIdx A

Tactic:
ramificationIdxIn_eq_ramificationIdx _ P (stabilizer Gal(L/K) P)

Goal state after:
case refine_3
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ P.ramificationIdx 𝓞D ≤ P.ramificationIdx A
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a.inl
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ j ∈ {n | 0 < n}

pp: case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ j ∈ {n | 0 < n}

Tactic:
· rw [Set.mem_ofPred_eq, ← hjk, beattySeq, Int.floor_pos]
      exact one_le_mul_of_one_le_of_one_le (by norm_cast) hrs.lt.le

Goal state after:
case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ j ∈ {n | 0 < n}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case left
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
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1

pp: case right
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
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1

Tactic:
· rw [← coePolynomial_eq_algebraMap]
    have hnπ : q % π ∉ {p : K[X] | v ↑p < 1 ∧ p ≠ 0} :=
      imp_not_comm.mp (degree_lt_wf.not_lt_min _) (EuclideanDomain.remainder_lt q hπ.2)
    have := Polynomial.valuation_le_one_of_valuation_X_le_one _ hle (q % π)
    grind

Goal state after:
case right
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
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
h : valuation K⟮X⟯ p = inftyValuation K
⊢ False

Tactic:
exact absurd Valuation.IsEquiv.refl (h ▸ adicValuation_not_isEquiv_infty_valuation p)

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
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
⊢ False

Tactic:
have hkltp := calc
          1 + k * k ≤ k * (k + 1) := by lia
          _ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)

Goal state after:
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
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
⊢ False
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ IsCoprime x n

Tactic:
rw [show y ^ 2 = n + -1 * x ^ 2 by lia] at hc2

Goal state after:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * 0
⊢ f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0

Tactic:
simpa [and_assoc] using hr

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

Goal state before:
pp: n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ (n ! * n + n !)

pp: case hb
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

pp: case hd
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
pow_add,

Goal state after:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ (n ! * n) * m ^ n !

case hb
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

case hd
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ (r + f.natDegree) * |x - ↑a / ↑b| < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
pow_add,

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * ↑b ^ f.natDegree * |x - ↑a / ↑b| < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: ⊢ IsGδ {x | Liouville x}

Tactic:
rw [setOfPred_liouville_eq_iInter_iUnion]
  refine .iInter fun n => IsOpen.isGδ ?_
  refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_
  exact isOpen_ball.inter isClosed_singleton.isOpen_compl

Goal state after:
Module: Mathlib.NumberTheory.Wilson

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

Tactic:
rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]

Goal state after:
Module: Mathlib.Order.Category.CompleteLat

Goal state before:
pp: α β : CompleteLat
e : ↑α ≃o ↑β
⊢ ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
      ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ } =
    𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
⊢ ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
⊢ InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
      InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) =
    𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ (ofAttributes r t).intent ⊆ c.intent ↔ t ⊆ c.intent

Tactic:
exact ⟨((subset_upperPolar_lowerPolar r t).trans ·),
    (isIntent_intent c).upperPolar_lowerPolar_subset⟩

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

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

Tactic:
apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
by
      suffices sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup P ⊓ sSup Q by simpa
      rw [sSup_inf_sSup]
      refine le_antisymm ?_ ?_
      · exact sSup_le fun a ⟨p, hp, q, hq, ha⟩ ↦ le_iSup₂_of_le (p, q) ⟨hp, hq⟩ <| by grind
      · exact iSup₂_le fun (p, q) ⟨hp, hq⟩ ↦ le_sSup_of_le ⟨p, hp, q, hq, rfl⟩ (by simp)

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

Goal state before:
pp: o : OrderType.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
rw [← @type_ne_zero_iff o.ToType, type_toType]

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
b : X
h1 : b ∈ a
h : ∀ x ∈ a, n x = x
⊢ n (sInf a) ≤ n b

Tactic:
exact n.monotone (sInf_le h1)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ Measurable (u i)

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ Measurable ((fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ Measurable fun p ↦ (fun i ω ↦ u (t i ω) ω) (↑p.1) p.2

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ Measurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable (u i)

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable fun p ↦ (fun i ω ↦ u (t i ω) ω) (↑p.1) p.2

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2))
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✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᵐ[μ] f n - f 0

Tactic:
simp only [predictablePart, ← Finset.sum_range_sub]

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i] =ᵐ[μ] ∑ i ∈ Finset.range n, (f (i + 1) - f i)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iic ↑(Order.pred i)
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
rw [this]

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iic ↑(Order.pred i)
⊢ MeasurableSet (τ ⁻¹' Set.Iic ↑(Order.pred i))
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
rw [this]

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

Goal state before:
pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ sInf {m} = m

pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ {m} ⊆ {i | u i ω ∈ s}

Tactic:
csInf_singleton

Goal state after:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ m = m

case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ {m} ⊆ {i | u i ω ∈ s}
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i ≤ τ ω}

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω < ↑i}ᶜ
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 τ
i : ι
this : {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i < τ ω}

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ ↑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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
rw [this]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
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:
rw [this]

Goal state after:
Ω : 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}ᶜ
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 : ι
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
have : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i} := by
    ext1 ω; simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, le_antisymm_iff]

Goal state after:
Ω : 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} ∩ {ω | τ ω ≥ ↑i}
⊢ MeasurableSet {ω | τ ω = ↑i}