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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }

Tactic:
have hdzne : F.derivative.aeval z ≠ 0 :=
    mt norm_eq_zero.2 (by rw [hz.1]; apply deriv_norm_ne_zero; assumption)

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ a.x - 1

Tactic:
sub_nonneg

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x
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✝²⁸ : 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
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
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
⊢ Module.IsTorsionFree 𝓞D B

Tactic:
Module.isTorsionFree_iff_faithfulSMul

Goal state after:
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✝²⁸ : 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
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
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
⊢ FaithfulSMul 𝓞D B
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
⊢ j ∉ {x | ∃ k, beattySeq' s k = x}

Tactic:
⟨m, h₂⟩

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hf
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hp : Nat.Prime p ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < s.nu p

Tactic:
apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case h_ne
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ d.primeFactors.Nonempty

Tactic:
· simp only [nonempty_primeFactors, show 1 < d by lia]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2

Tactic:
use 1, 0, 1; simp

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

Goal state before:
pp: case refine_2
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
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L

Tactic:
have b''_sp : Submodule.span K (Set.range b'') = ⊤ := ?_

Goal state after:
case refine_2.refine_2
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
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
b''_sp : Submodule.span K (Set.range b'') = ⊤
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L

case refine_2.refine_1
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
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
⊢ Submodule.span K (Set.range b'') = ⊤
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : (norm a).natAbs = p
⊢ a.re.natAbs ^ 2 + a.im.natAbs ^ 2 = p

Tactic:
simpa [natAbs_norm_eq, sq] using hnap

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

Goal state before:
pp: case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasureTheory.volume (Set.Ioc 0 1) < ⊤

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

Tactic:
· rw [Real.volume_Ioc, sub_zero]; exact ENNReal.ofReal_lt_top

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

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

Tactic:
change 1 ≤ (a + 1 : ℝ) ^ f.natDegree * |eval α fR - eval ((z : ℝ) / (a + 1)) fR|

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

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith q x

Tactic:
refine ⟨C, hC.mono ?_⟩

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (-x)

Tactic:
refine ⟨C, hC.mono ?_⟩

Goal state after:
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j = (ConcreteCategory.hom (s.π.app { as := j })) t

Tactic:
← w ⟨j⟩

Goal state after:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j = (ConcreteCategory.hom (m ≫ (product f).π.app { as := j })) t
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
⊢ b ≤ a

Tactic:
obtain ⟨t, hts, ht_ne, ht_c, ht_lub⟩ := hb

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
t : Set α
hts : t ⊆ s
ht_ne : t.Nonempty
ht_c : t.Countable
ht_lub : IsLUB t b
⊢ b ≤ a
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
by
  unfold RTendsto' rcomap'; constructor
  · simpa [le_def, SetRel.mem_image] using fun h s hs => h _ _ hs Set.Subset.rfl
  · simpa [le_def, SetRel.mem_image] using fun h s t ht => mem_of_superset (h t ht)

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: case mp
α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r → s.Nonempty

Tactic:
· intros
    by_contra! hh
    simp_all

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: case mpr
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.Nonempty → 1 ≤ s.chainHeight r

Tactic:
· intros
    by_contra! hh
    simp_all

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
⊢ ∃ f, P.IsRepFun f

Tactic:
by
  obtain ⟨f, hf, -⟩ := exists_extend_partial' P (t := ∅) (by simp)
  exact ⟨f, hf⟩

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

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ lift.{u_1, u} (type α) = lift.{u_1, u} (type β) ↔ Nonempty (α ≃o β)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h⟩ ↦ congrArg lift <| type_congr h⟩

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)
⊢ Nonempty (α ≃o β)
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
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
⊢ Martingale g ℱ μ

Tactic:
by
  refine ⟨hg, fun i j hij ↦ ?_⟩
  calc μ[g j | ℱ i] =ᵐ[μ] μ[f j | ℱ i] := (condExp_congr_ae (h_eq j)).symm
    _ =ᵐ[μ] g i := (hf.2 i j hij).trans (h_eq i)

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

Goal state before:
pp: case pos
Ω : 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
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

pp: case neg
Ω : 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
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

Tactic:
· rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]
        let : MeasurableSpace Ω := 𝓕 n
        exact ((h n).approx m).measurableSet_fiber s

Goal state after:
case neg
Ω : 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
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
Module: Mathlib.Probability.Martingale.Basic

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

Tactic:
by
  rw [← neg_neg f]
  refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg
  simpa only [Pi.zero_apply, Pi.neg_apply, neg_sub_neg]

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

Goal state before:
pp: case zero
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
⊢ upperCrossingTime a b f N 0 ω ≤ N

pp: case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N

Tactic:
· simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]

Goal state after:
case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  0 ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
sub_nonneg

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (f n - f 0) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
integral_sub' (hf.integrable _) (hf.integrable _),

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (a : Ω), f n a ∂μ - ∫ (a : Ω), f 0 a ∂μ ≤ ∫ (a : Ω), f n a ∂μ - ∫ (a : Ω), f 0 a ∂μ
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₂ ω
⊢ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω

Tactic:
refine lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) ?_)
  rw [Set.mem_ofPred_eq, upperCrossingTime_succ_eq, hittingBtwn_lt_iff _ le_rfl]
  refine ⟨N₂, ⟨?_, Nat.lt_succ_self _⟩, hN₂'.le⟩
  rw [lowerCrossingTime, hittingBtwn_le_iff_of_lt _ (Nat.lt_succ_self _)]
  refine ⟨N₁, ⟨le_trans ?_ hN₁, hN₂⟩, hN₁'.le⟩
  by_cases! hN : 0 < N
  · have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
      Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab)
    rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _))
      this]
    exact this.le
  · rw [Nat.le_zero] at hN
    rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']

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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f (↑N).untopA ω - f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω

Tactic:
sub_nonneg

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω ≤ f (↑N).untopA ω
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (fun ω ↦ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω)
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

Tactic:
refine Integrable.integrableOn ?_
        refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)
        exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici

Goal state after:
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 ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 ≤ rexp (t * X x)

Tactic:
exact (exp_pos _).le

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t

Tactic:
by
  rw [mgf, integral_smul_measure, mgf, smul_eq_mul]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (fun ω ↦ rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
simp_rw [mgf, Pi.add_apply, mul_add, exp_add]
  exact (h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY

Goal state after: