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

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

Tactic:
rw [sub_nonneg]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x
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
⊢ Tendsto (fun n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)

Tactic:
by
  rw [← mul_zero ‖F.derivative.aeval a‖, sq]
  simp only [mul_assoc]
  apply Tendsto.mul
  · apply tendsto_const_nhds
  · apply bound'
    assumption

Goal state after:
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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ T_gen p F a > 0

Tactic:
T_def

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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 > 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case hH.refine_2
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
kb : ℤ
hab : v ↑πᵥ ^ ka * ↑γ = v ↑πᵥ ^ kb
hkb : v b = v ↑πᵥ ^ kb
⊢ ∃ k, ⋯.unit ^ k = γ

Tactic:
use kb - ka

Goal state after:
case h
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
kb : ℤ
hab : v ↑πᵥ ^ ka * ↑γ = v ↑πᵥ ^ kb
hkb : v b = v ↑πᵥ ^ kb
⊢ ⋯.unit ^ (kb - ka) = γ
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ 0 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
grw [sq_nonneg (∑ d ∈ n.divisors, weights d), sum_divisors_lambda_sq_larger_sum _ n, sum_comm]

Goal state after:
case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ (∑ d ∈ n.divisors, weights d) ^ 2 ≤
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p
⊢ 0 < k * ↑p

Tactic:
← hk

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p
⊢ 0 < ↑a ^ 2 + ↑b ^ 2 + 1
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ↑(f 0) ^ 2 + ↑(f 1) ^ 2 + ↑(f 2) ^ 2 + ↑(f 3) ^ 2 = 0

Tactic:
by
    rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
    simp only [Int.cast_add, Int.cast_pow]
    rfl

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

Goal state before:
pp: p : ℂ[X]
s : ℂ
x : ℝ
⊢ HasDerivAt (fun x ↦ -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
have h₀ := (hasDerivAt_id' x).smul_const s

Goal state after:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y ↦ y • s) (1 • s) x
⊢ HasDerivAt (fun x ↦ -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p

Tactic:
obtain ⟨c', hc', h'⟩ := P_le_aux f s c hc; clear c hc
  let c₁ := max (Real.exp s.re) 1
  let c₂ := max (Real.exp ‖s‖) 1
  let c₃ := max ‖s‖ 1
  use c₁ * (c₂ * c' * c₃), by positivity
  intro p hp
  refine (h' p).trans ?_
  simp_rw [mul_pow]
  have le_max_one_pow {x : ℝ} : x ≤ max x 1 ^ p :=
    (max_cases x 1).elim (fun h ↦ h.1.symm ▸ le_self_pow₀ h.2 hp)
      fun h ↦ by rw [h.1, one_pow]; exact h.2.le
  gcongr <;> exact le_max_one_pow

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

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ C < ↑n ^ (-q) * ↑n ^ p

Tactic:
rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]

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

Goal state before:
pp: p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x

Tactic:
by
  rw [mul_comm, mul_nat_iff hn]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

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

pp: case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, ↑a = ↑(↑a).val

Tactic:
· intro b hb
    rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
    refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
    · intro h; apply hb.1; apply_fun val at h
      simpa only [val_cast_of_lt hb.right, val_zero] using h
    · simp only [val_cast_of_lt hb.right, Units.val_mk0]

Goal state after:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, ↑a = ↑(↑a).val
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ 0 < a + 1 ∧ a < ↑b + 1

Tactic:
← neg_lt_iff_pos_add,

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ -1 < a ∧ a < ↑b + 1
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : e ∈ lowerBounds s
⊢ e ≤ sInf s

Tactic:
by_contra! hs
    obtain ⟨a, ha⟩ := hs
    refine ha.2.not_ge <| le_sInf_apply fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
    simp_all

Goal state after:
Module: Mathlib.Order.CompleteSublattice

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

Tactic:
iSup,

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ principal a < principal b ↔ a < b

Tactic:
simp [lt_iff_le_not_ge]

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
⊢ (⨆ i, f i).extent = lowerPolar r (⋂ i, (f i).intent)

Tactic:
iSup,

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

Tactic:
iSup,

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

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB A (x, y)
⊢ (x, y) ∈ s ×ˢ t

Tactic:
isLUB_prod

Goal state after:
α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ (x, y) ∈ s ×ˢ t
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain (flip r) a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ r x y ∨ r y x) x✝¹ x✝

Tactic:
simpa [flip, Or.comm] using ha₃ hx hy hne

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ flip r x y ∨ flip r y x) x✝¹ x✝

Tactic:
simpa [flip, Or.comm] using ha₃ hx hy hne

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
⊢ grade ℕ (f i) = i

Tactic:
induction i with
  | zero => simp [h0]
  | succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ {x_1 | ∃ i ∈ I, ∃ j ∈ principal x, x_1 = i ⊔ j}
⊢ y ∈ I

Tactic:
rcases hyJ with ⟨a, ha, b, hb, hy⟩

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ y ∈ I
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ↑(a ⊓ sSup s) ≤ ↑(⨆ x, a ⊓ ↑x)

Tactic:
iSup,

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ↑(a ⊓ sSup s) ≤ ↑(sSup (range fun x ↦ a ⊓ ↑x))
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_1
α : 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
e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d)
⊢ IsLUB ({f a} ×ˢ (g '' d)) (f a, g c)

Tactic:
exact .prod (singleton_nonempty _) (hd₁.image _) isLUB_singleton (hg hd₁ hd₂ hdc)

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

Goal state before:
pp: case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)

Tactic:
push Not at h

Goal state after:
case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ∀ (b : ↑t), ¬P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α * 1 = type α

Tactic:
by
      simp only [show 1 = type PUnit by rfl, ← type_lex_prod]
      exact (Prod.Lex.uniqueProd PUnit α).type_congr

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✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

Tactic:
by
  rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
  refine setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_
  filter_upwards [hf.2.1 i j hij] with _ heq using heq

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ (i : ℕ),
      ‖∑ c ∈ Finset.range (i + 1), μ[f (c + 1) - f c | ↑ℱ c] ω - ∑ c ∈ Finset.range i, μ[f (c + 1) - f c | ↑ℱ c] ω‖ ≤ R

Tactic:
Finset.sum_range_succ_sub_sum

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖μ[f (i + 1) - f i | ↑ℱ i] ω‖ ≤ R
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_
  simp only [stoppedValue]
  rw [← h]
  exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N n ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N n ω)

Tactic:
induction n with
  | zero =>
    refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
  | succ k ih =>
    have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]
    refine ⟨this, fun n ↦ ?_⟩
    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
    simp [upperCrossingTime_le]

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

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

Tactic:
hittingBtwn_le_iff_of_exists h_exists

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (∃ j ∈ Set.Icc n i, u j ω ∈ s) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
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₂ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a

Tactic:
refine ⟨N₁, ⟨le_trans ?_ hN₁, hN₂⟩, hN₁'.le⟩

Goal state after:
Ω : 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
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:
rw [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.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:
rw [sub_nonneg]
            exact le_trans (stoppedValue_lowerCrossingTime heq) hf

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ IsPiSystem (⋃ i, {x | MeasurableSet x})

Tactic:
exact isPiSystem_iUnion_of_monotone _ (fun n ↦ (ℱ n).isPiSystem_measurableSet) fun _ _ ↦ ℱ.mono

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω ↦ ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
i : ℕ
x✝ : i ∈ Finset.Ico 1 (N + 1)
⊢ MeasurableSet fun ω ↦ {n | upperCrossingTime a b f N n ω < N} i

Tactic:
simpa only [ENat.some_eq_natCast, Nat.cast_lt] using!
    hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N

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}) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})

Tactic:
IsStoppingTime.measurableSpace_const,

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}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
n : ℕ
⊢ 0 ≤ ∑ x ∈ Finset.range (n + 1), μ.real (s (x + 1)) - ∑ x ∈ Finset.range n, μ.real (s (x + 1))

Tactic:
Finset.sum_range_succ_sub_sum

Goal state after:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
n : ℕ
⊢ 0 ≤ μ.real (s (n + 1))