mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

pp: case inr
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hge : v X ≤ 1
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

Tactic:
· have hv := valuation_isEquiv_inftyValuation_of_one_lt_valuation_X hlt
    refine .inl ⟨hv, ?_⟩
    simp only [ExistsUnique, not_exists, not_and, not_forall]
    intro pw hw
    exact absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)

Goal state after:
case inr
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hge : v X ≤ 1
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: ⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp [div_def]; rfl

Goal state after:
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
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
y' : S
hy' : y' ∈ span {a}
z : S
hz : z ∈ P ^ (i + 1)
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : y' + z ∈ P ^ i
hx' : y' + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z), hx✝⟩

Tactic:
obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hy'

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
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel
        ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z), hx✝⟩
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q

Tactic:
div_sub_div _ _ b0 qR0.ne',

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |(↑a * ↑q - ↑b * ↑p) / (↑b * ↑q)| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

Tactic:
have ar : α ∈ (fR.roots.toFinset : Set ℝ) :=
    Finset.mem_coe.mpr (Multiset.mem_toFinset.mpr ((mem_roots fR0).mpr (IsRoot.def.mpr fa)))

Goal state after:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
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
p : Ideal R
hp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
P : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
        rw [IsDedekindDomain.ramificationIdx'_eq_factors_count hp (Factors.isPrime p P)
            (Factors.ne_bot p P)]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ n ∣ (n - 1)! + 1

Tactic:
rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b | ¬r b a} → r b_1 b
⊢ Bounded r s

Tactic:
obtain ⟨m, hm⟩ := H a b

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b | ¬r b a} → r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s
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:
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:
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:
ext; exact e.symm_apply_apply _

Goal state after:
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
this : x ⊔ y = sSup {x, y}
z : α
hz : z ∈ {x, y}
⊢ z ∈ carrier

Tactic:
aesop

Goal state after:
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
this : x ⊓ y = sInf {x, y}
z : α
hz : z ∈ {x, y}
⊢ z ∈ carrier

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ lowerPolar r (⋂ i ∈ range fun i ↦ f i, i.intent) = lowerPolar r (⋂ i, (f i).intent)

Tactic:
← Set.iInf_eq_iInter,

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ ⋂ i ∈ range fun i ↦ f i, i.intent = ⋂ i, (f i).intent

Tactic:
← Set.iInf_eq_iInter,

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

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

Tactic:
← Set.iInf_eq_iInter,

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ ⨅ i ∈ range fun i ↦ f i, 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
⊢ upperPolar r (⋂ i ∈ range fun i ↦ f i, i.extent) = upperPolar r (⋂ i, (f i).extent)

Tactic:
← Set.iInf_eq_iInter,

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

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
x : α
s : Set α
y : α
hy : IsLUB {x} y
h_eq : s = {x}
⊢ y = x

Tactic:
exact IsLUB.unique hy isLUB_singleton

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ hb.rank

Tactic:
rw [hb.rank_eq]

Goal state after:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ ⨆ b_1, Order.succ ⋯.rank
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
⊢ cocardinal α isRegular_aleph0 = cofinite

Tactic:
aesop

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #↑S < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ ∀ (i : ↑(compl '' S)), #↑↑i < c

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b : Regular α
c : α
⊢ c ⊓ ↑a ≤ ↑b ↔ Disjoint (↑b)ᶜ (c ⊓ ↑a)

Tactic:
b.prop.disjoint_compl_left_iff

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b : Regular α
c : α
⊢ c ⊓ ↑a ≤ ↑b ↔ c ⊓ ↑a ≤ ↑b
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ f i ≤ f j

pp: case refine_2
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ g i ≤ g j

pp: case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s

Tactic:
· obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le

Goal state after:
case refine_2
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ g i ≤ g j

case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (y ⊓ x) ≤ n y

Tactic:
gcongr; exact inf_le_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
⊢ (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
⊢ (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}

Tactic:
aesop

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
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ Tendsto (fun l p ↦ U l (↑p.1) p.2) fltr (𝓝 fun p ↦ u (↑p.1) p.2)

Tactic:
rw [tendsto_pi_nhds] at h_tendsto ⊢

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun i ↦ U i x) fltr (𝓝 (u x))
i : ι
⊢ ∀ (x : ↑(Set.Iic i) × Ω), Tendsto (fun i_1 ↦ U i_1 (↑x.1) x.2) fltr (𝓝 (u (↑x.1) x.2))
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ {ω | (n + 1, ω) ∈ s} = Prod.mk ⟨n + 1, ⋯⟩ ⁻¹' (fun p ↦ (↑p.1, p.2)) ⁻¹' s

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : ↑(Set.singleton (n + 1)) × Ω
hp2 : p.2 ∈ A
x✝ : i < n + 1
⊢ p.1 = ⟨n + 1, ⋯⟩

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ MeasurableSpace.comap (fun x ↦ (↑x.1, x.2)) 𝓕.predictable ≤ Subtype.instMeasurableSpace.prod (↑𝓕 i)

Tactic:
refine MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)

case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ ∀ (i_1 : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i_1 ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = {⊥} ×ˢ A

Tactic:
aesop

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

Goal state before:
pp: Ω : 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 : ℕ
s : E
⊢ X m ⁻¹' {s} = {ω | (n + 1, ω) ∈ ⇑(StronglyMeasurable.approx h𝓕 m) ⁻¹' {s}}

Tactic:
aesop

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 : ℕ
⊢ ∀ (y : Ω), X m y ∈ Set.range ⇑(StronglyMeasurable.approx h𝓕 m)

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ Y m ⁻¹' {s} = ⋃ n, {n} ×ˢ (Function.curry (Y m) n ⁻¹' {s})

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : n + 1 ≤ m
⊢ Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1)

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ Function.curry (Y m) (n + 1) = Function.curry (X m) 0

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ (↑(Finset.range (m + 1))).Finite

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
i j : ι
hij : i ≤ j
⊢ g i ≤ᵐ[μ] μ[g j | ↑ℱ i]

Tactic:
exact (Filter.eventuallyLE_congr (h_eq i) (condExp_congr_ae (h_eq j))).mp (ae_le_condExp hf hij)

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ (if n ≤ m then n else 0) ∈ Finset.range (m + 1)

Tactic:
aesop

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ Function.curry (X m) (if n ≤ m then n else 0) ω = e

Tactic:
aesop

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

Goal state before:
pp: case refine_2
Ω : 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])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ k]

Tactic:
· rw [condExp_of_stronglyMeasurable]
      · exact stronglyMeasurable_condExp.mono (ℱ.mono hk.le)
      · exact integrable_condExp

Goal state after: