mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖ ≤ ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
by
      apply mul_le_of_le_one_left (norm_nonneg _)
      simpa only [← coe_intCast] using norm_le_one _

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g g' : C(Y, R)
⊢ f.comp fst * (g + g').comp snd = f.comp fst * g.comp snd + f.comp fst * g'.comp snd

Tactic:
by ext; simp [mul_add]

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]

Tactic:
rw [← this] at hdiv

Goal state after:
case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : k ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ a = 1 ∨ a = -1 ↔ a.y = 0

Tactic:
by
  refine ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => ?_⟩
  have prop := a.prop
  rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop
  exact prop.imp (fun h => ext h H) fun h => ext h H

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: 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✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : MulSemiringAction Gal(L/K) B
inst✝⁹ : IsGaloisGroup Gal(L/K) A B
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Ring.HasFiniteQuotients A
inst✝³ : P.IsMaximal
D : Type u_5
inst✝² : Field D
inst✝¹ : Algebra D L
inst✝ : IsDecompositionField K L P D
hp : p ≠ ⊥
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B

Tactic:
by
  have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have : Finite (A ⧸ p) := Ring.HasFiniteQuotients.finiteQuotient hp
  rw [← IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L, card_stabilizer_eq p]

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
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x : S
hx : x ∈ Submodule.restrictScalars R (S ∙ f A.det)
⊢ x ∈ M

Tactic:
rw [Submodule.restrictScalars_mem] at hx

Goal state after:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x : S
hx : x ∈ S ∙ f A.det
⊢ x ∈ M
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ exp (-↑(multiplicity v.asIdeal (Ideal.span {x}))) ^ v.asIdeal.ramificationIdx' w.asIdeal =
    exp (-↑(multiplicity w.asIdeal (Ideal.span {(algebraMap A B) x})))

Tactic:
← Set.image_singleton,

Goal state after:
case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ exp (-↑(multiplicity v.asIdeal (Ideal.span {x}))) ^ v.asIdeal.ramificationIdx' w.asIdeal =
    exp (-↑(multiplicity w.asIdeal (Ideal.span (⇑(algebraMap A B) '' {x}))))
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ emultiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x})) =
    ↑(v.asIdeal.ramificationIdx' w.asIdeal * multiplicity v.asIdeal (Ideal.span {x}))

Tactic:
replace hx : Ideal.span {x} ≠ ⊥ := by simp [hx]

Goal state after:
case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : Ideal.span {x} ≠ ⊥
⊢ emultiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x})) =
    ↑(v.asIdeal.ramificationIdx' w.asIdeal * multiplicity v.asIdeal (Ideal.span {x}))
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⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < b.degree
⊢ ↑a.natDegree < ↑a.natDegree + b.degree

Tactic:
degree_eq_natDegree hab.2.2

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < ↑b.natDegree
⊢ ↑a.natDegree < ↑a.natDegree + ↑b.natDegree
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ n = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Tactic:
by rw [h, h₃, h₄]; ring

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x1 x2 ↦ x1 < x2) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b

Tactic:
simp only [Unbounded, not_lt]

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ L M : CompleteSublattice α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
cases L; cases M; congr; exact SetLike.coe_injective h

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
⊢ ⨆ n, A n ∈ s

Tactic:
by
  let i₀ := Nonempty.some (α := ι) inferInstance
  exact hs.isLUB_mem (range A) (by simp [range]; grind) ⟨A i₀, by simp⟩ (countable_range A) _
    isLUB_iSup

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

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter α
inst✝ : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (map f l) c

Tactic:
by
  refine ⟨fun S hSc hS => ?_⟩
  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
  exact (cardinal_bInter_mem hSc).2 hS

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ s.chainHeight r ≤ t.chainHeight r

Tactic:
refine forall_natCast_le_iff_le.mp fun n hn ↦ ?_
  obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
  exact ha₂ ▸ encard_le_chainHeight_of_isChain _ _ (ha₁.trans h) ha₃

Goal state after:
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]

Goal state after:
α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ ↑P, a
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB (range fun a ↦ (fun b ↦ f (↑a, b)) (p1, p2).2) (f (p1, p2))

Tactic:
Set.range

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB {x | ∃ y, (fun b ↦ f (↑y, b)) (p1, p2).2 = x} (f (p1, p2))
Module: Mathlib.Order.UpperLower.Prod

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

Tactic:
prod_eq_bot

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
rw [← Set.Ioi_sdiff_Ioi, (by simp : (Set.Ioi i \ Set.Ioi j) ×ˢ s
      = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s), ← Set.prod_sdiff_prod]
    exact (measurableSet_predictable_Ioi_prod hs).diff
      (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)

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
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f ⊔ g) i ≤ᵐ[μ] μ[(f ⊔ g) j | ↑ℱ i]

Tactic:
refine EventuallyLE.sup_le ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁸ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᵐ[μ] μ[(f ⊔ g) j | ↑ℱ i]

case refine_2
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁸ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᵐ[μ] μ[(f ⊔ g) j | ↑ℱ i]
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_3.succ
Ω : 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_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
ω : Ω
n : ℕ
⊢ Tendsto (fun m ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))

Tactic:
· exact (h n).tendsto_approx ω

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 : ι
ω : Ω
inst✝ : WellFoundedLT ι
hl : hittingAfter u s n ω ≠ ⊤
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
by
  simp only [ne_eq, hittingAfter_eq_top_iff, not_forall, not_not] at hl
  obtain ⟨j, hj₁, hj₂⟩ := hl
  exact hittingAfter_mem_set ⟨j, hj₁, hj₂⟩

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
by_cases! hN : 0 < N

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N ≤ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
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
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))

Tactic:
by
  classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩

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

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

Tactic:
obtain ⟨m, hm⟩ := exists_nat_ge k
    refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
    rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]

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

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

Tactic:
rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
    IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ (MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑i_1})) ↔
    (MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑i_1})) ∧
      MeasurableSet (s ∩ {ω | τ ω ≤ ↑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✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : {ω | τ ω = π ω} = {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω}
⊢ MeasurableSet {ω | π ω ≤ τ ω}

Tactic:
convert! (measurableSet_stopping_time_le_min hπ hτ) using 3

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ 0 < ∫ (x : Ω), rexp (t * X x) ∂μ

Tactic:
have : ∫ x : Ω, exp (t * X x) ∂μ = ∫ x : Ω in Set.univ, exp (t * X x) ∂μ := by
    simp only [Measure.restrict_univ]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < ∫ (x : Ω), rexp (t * X x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ mgf X (Measure.map Y μ) t = mgf (X ∘ Y) μ t

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ ∫ (x : Ω), rexp (t * X x) ∂Measure.map Y μ = ∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf X μ = mgf Y μ'

Tactic:
rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ mgf (-X) μ t = mgf X μ (-t)

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ ∫ (x : Ω), rexp (t * (-X) x) ∂μ = ∫ (x : Ω), rexp (-t * X x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (α • X) μ t = mgf X μ (α * t)

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * (α • X) x) ∂μ = ∫ (x : Ω), rexp (α * t * X x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω ↦ α + X ω) μ t = rexp (t * α) * mgf X μ t

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (α + X ω))) x ∂μ = rexp (t * α) * mgf X μ t
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (α + X ω))) x ∂μ = rexp (t * α) * mgf X μ t

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (α + X ω))) x ∂μ = rexp (t * α) * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (fun ω ↦ rexp (t * X ω)) μ
hν : Integrable (fun ω ↦ rexp (t * X ω)) ν
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (fun ω ↦ rexp (t * X ω)) μ
hν : Integrable (fun ω ↦ rexp (t * X ω)) ν
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t