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

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ ∃ a, IsFundamental a

Tactic:
refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ (Solution₁.mk (↑x₁) y₁ hy₁).x ≤ b.x
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < ↑j
h₄ : ↑j + ↑1 < ↑k + ↑1 + (↑m + ↑1)
⊢ False

Tactic:
← add_assoc,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < ↑j
h₄ : ↑j + ↑1 < ↑k + ↑1 + ↑m + ↑1
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑(⌈(↑j + 1) / r⌉ - 1) < ↑j / r ∧ (↑j + 1) / r ≤ ↑(⌈(↑j + 1) / r⌉ - 1) + 1

Tactic:
Int.cast_sub,

Goal state after:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑⌈(↑j + 1) / r⌉ - ↑1 < ↑j / r ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉ - ↑1 + 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ ↑(⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑(⌈(↑j + 1) / r⌉ - 1) * r < ↑j + 1

Tactic:
Int.cast_sub,

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - ↑1) * r ∧ (↑⌈(↑j + 1) / r⌉ - ↑1) * r < ↑j + 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1

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

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
⊢ ∑ i ∈ l.divisorsAntidiagonal, (s.nu l)⁻¹ * (↑(μ i.1) * s.nu i.1) =
    ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹

Tactic:
congr! 1 with ⟨d, e⟩ hd

Goal state after:
case a
s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
d e : ℕ
hd : (d, e) ∈ l.divisorsAntidiagonal
⊢ (s.nu l)⁻¹ * (↑(μ (d, e).1) * s.nu (d, e).1) = ↑(μ (d, e).1) * (s.nu (d, e).2)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms d / selbergTerms l = selbergTerms d * (selbergTerms l)⁻¹

pp: case a.hl
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ (d / l).Coprime l

pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
· ring

Goal state after:
case a.hl
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ (d / l).Coprime l

case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ w d1 * w d2 * (s.nu d1 * s.nu d2 / s.nu (d1.gcd d2)) = s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ s.nu (d1.gcd d2) ≠ 0

Tactic:
· ring

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ s.nu (d1.gcd d2) ≠ 0
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
rw [ha, hb]; ring

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2

Tactic:
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb

Goal state after:
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hn

Goal state after:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ q ∈ n.primeFactors, q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3

Tactic:
replace hp := H _ <|
      Nat.mem_primeFactors.mpr ⟨hp, dvd_of_mul_right_dvd hpq, Squarefree.ne_zero hn⟩
    replace hq := hq (dvd_of_mul_left_dvd hpq)
    rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢
    rw [Nat.cast_mul]
    exact help p q hp hq

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
      obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
      exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring,
        ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ e (C ↑p) = C ↑p

Tactic:
rw [OrderIso.apply_blimsup e, ← hu₀ p]

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ (blimsup (⇑e ∘ X) atTop fun n ↦ 0 < n ∧ addOrderOf (u p) ^ 2 ∣ n) = C (addOrderOf (u p))
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: case right
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I)ᶜ

Tactic:
refine .of_def ?_ ?_ ?_

Goal state after:
case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ (↑I)ᶜ.Nonempty

case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) (↑I)ᶜ

case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩
  · apply le_antisymm
    · simp only [iSup_le_iff]
      exact h a ha
    · apply le_iSup₂ b hb
  · apply le_antisymm
    · apply iInf₂_le a ha
    · simp only [le_iInf_iff]
      intro x hx
      exact h x hx b hb
  · trans f a b
    · -- f a y ≤ f a b
      rw [← h]
      apply le_iSup₂ y hy
    · -- f a b ≤ f x b
      rw [← h']
      apply iInf₂_le x hx

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := ⋯
bJ : b ∈ J
⊢ b₁ ≤ b

pp: case h₁
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := ⋯
bJ : b ∈ J
⊢ b₂ ≤ b

Tactic:
exacts [le_sup_left, le_sup_right]

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

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

Tactic:
ext1 ω

Goal state after:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ ∅
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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
⊢ StronglyAdapted ℱ fun n ↦ h (n + 1)

Tactic:
rw [hh]

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
⊢ StronglyAdapted ℱ fun n ↦ (predictablePart (f + g) ℱ μ - g) (n + 1)
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
ext1 ω

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

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

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i < τ ω} ↔ ω ∈ {ω | τ ω ≤ ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
⊢ {ω | τ ω < ↑i} = ∅

Tactic:
ext1 ω

Goal state after:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ ∅
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
⊢ {ω | τ ω < ↑i} = τ ⁻¹' Set.Iio ↑i

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ τ ⁻¹' Set.Iio ↑i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = ↑i} ↔ ω ∈ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
a : ι
⊢ ↑a ≤ ↑i ↔ ∃ i_1 ≤ i, ↑a = ↑i_1

Tactic:
| coe a =>

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

Goal state before:
pp: case h₁
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ BddAbove {n | upperCrossingTime a b f M n ω < M}

Tactic:
exact upperCrossingTime_lt_bddAbove hab

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ f (upperCrossingTime a b f N (k + 1) ω) ω - f 0 ω + -(f (lowerCrossingTime a b f N k ω) ω - f 0 ω) =
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω

pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
neg_sub,

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ f (upperCrossingTime a b f N (k + 1) ω) ω - f 0 ω + (f 0 ω - f (lowerCrossingTime a b f N k ω) ω) =
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω

Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
⊢ a + i ≤ j ↔ a ≤ j - i

Tactic:
simp_rw [← le_sub_iff_add_le]

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
⊢ ↑a + ↑i ≤ ↑j ↔ ↑a ≤ ↑(j - i)

Tactic:
| coe a =>

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
a : ι
⊢ ↑a + ↑i ≤ ↑j ↔ ∃ i_1, ↑a = ↑↑i_1

Tactic:
| coe a =>

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
a : ι
⊢ ↑a + π ω ≤ ↑j ↔ ∃ i, π ω = ↑↑i ∧ ↑a + ↑↑i ≤ ↑j

Tactic:
| coe a =>

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
⊢ {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
⊢ ω ∈ {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑j} ↔ ω ∈ {ω | τ ω ≤ ↑(min i j)}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | ↑i ≤ τ ω} = {ω | τ ω = ↑i} ∪ {ω | ↑i < τ ω}

Tactic:
ext1 ω

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω = ↑i} ∪ {ω | ↑i < τ ω}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
⊢ i < a ∨ a = i ↔ a = i ∨ i < a

Tactic:
or_comm

Goal state after:
case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
a : ι
⊢ a = i ∨ i < a ↔ a = i ∨ i < a