mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
S : Set (X × X)
inst✝² : CompactSpace X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ n D,
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧ univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Disjoint on D)

Tactic:
obtain ⟨t, U, hUc, hUS⟩ := exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact hS
  -- Now refine it to a disjoint covering.
  obtain ⟨n, W, hW₁, hW₂, hW₃⟩ := hUc.exists_finite_nonempty_disjoint_clopen_cover
  refine ⟨n, W, fun j ↦ (hW₁ j).1, fun j y hy z hz ↦ ?_, hW₂, hW₃⟩
  exact match (hW₁ j).2 with | ⟨i, hi⟩ => hUS i ⟨hi hy, hi hz⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |√↑d + ↑q| * |√↑d - ↑q| < ↑M * (1 / ↑q.den ^ 2)

Tactic:
refine mul_lt_mul'' (((abs_add_le ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |ξ| + |↑q| ≤ 2 * |ξ| + 1
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]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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⟩
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ (2 ^ n * 2) =
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)

Tactic:
pow_succ 2

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]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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⟩
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ (2 ^ n * 2) =
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ (2 ^ n * 2)
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
n : ℕ
⊢ ‖↑(newton_seq_aux hnorm (n + 1)) - ↑(newton_seq_aux hnorm n)‖ =
    ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) F‖ /
      ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖

Tactic:
newton_seq_aux,

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
n : ℕ
⊢ ‖↑(ih_n hnorm ⋯) - ↑(newton_seq_aux hnorm n)‖ =
    ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) F‖ /
      ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d =
    s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d

Tactic:
rw [mainSum, mul_sum, ← sum_add_distrib]
    congr with d
    rw [rem]
    ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: weights : ℕ → ℝ
hw : weights 1 = 1
⊢ IsUpperMoebius (lambdaSquared weights)

Tactic:
dsimp only [IsUpperMoebius, lambdaSquared]
  intro n
  split_ifs
  · simp_all
  grw [sq_nonneg (∑ d ∈ n.divisors, weights d), sum_divisors_lambda_sq_larger_sum _ n, sum_comm]
  apply le_of_eq
  simp_rw [sq, mul_sum, sum_mul]
  congr! 1 with d1 hd1
  rw [sum_comm]
  congr! 1 with d2 hd2
  rw [sum_ite_eq_of_mem', mul_comm]
  -- Deal with the side goal from `sum_ite_eq_of_mem'`
  rw [mem_divisors, Nat.lcm_dvd_iff]
  exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ selbergTerms.IsMultiplicative

Tactic:
unfold selbergTerms
  arith_mult

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬((↑p).natAbs = 1 ∧ (↑p).natAbs = 1)

Tactic:
exact fun h => (ne_of_lt hp.1.one_lt).symm h.1

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case pos
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d m : ℕ
hmin : ∀ m_1 < 2 * m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd : ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2 = 2 * (↑m * ↑p)
w✝³ w✝² w✝¹ w✝ : ℤ
h : w✝³ ^ 2 + w✝² ^ 2 + w✝¹ ^ 2 + w✝ ^ 2 = ↑m * ↑p
⊢ False

Tactic:
exact hmin m hm₂ ⟨hm₂.trans hmp, hm₀, _, _, _, _, natAbs_iff.2 h⟩

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ False

Tactic:
by
      let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 hp3
      obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
        exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩
      have hpk : p ∣ k ^ 2 + 1 := by
        rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
          ← hk, neg_add_cancel]
      have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by ext <;> simp [sq]
      have hk₀ : k ≠ 0 := by rintro rfl; simp at hk
      have hkltp := calc
          1 + k * k ≤ k * (k + 1) := by lia
          _ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)
      have hpk₁ : ¬(p : ℤ[i]) ∣ ⟨k, -1⟩ := fun ⟨x, hx⟩ =>
        lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
          calc
            (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, -1⟩).natAbs := by rw [hx]
            _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using! hkltp
            _ ≤ (norm (p * x : ℤ[i])).natAbs :=
              norm_le_norm_mul_left _ fun hx0 =>
                show (-1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using! congr_arg Zsqrtd.im hx
      have hpk₂ : ¬(p : ℤ[i]) ∣ ⟨k, 1⟩ := fun ⟨x, hx⟩ =>
        lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
          calc
            (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, 1⟩).natAbs := by rw [hx]
            _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using! hkltp
            _ ≤ (norm (p * x : ℤ[i])).natAbs :=
              norm_le_norm_mul_left _ fun hx0 =>
                show (1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using! congr_arg Zsqrtd.im hx
      obtain ⟨y, hy⟩ := hpk
      have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
      tauto

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

Goal state before:
pp: case refine_1
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ ((e - j).pred + 1) • Module.rank (R ⧸ p) (S ⧸ P) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)

pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥

Tactic:
← Nat.succ_eq_add_one,

Goal state after:
case refine_1
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ (e - j).pred.succ • Module.rank (R ⧸ p) (S ⧸ P) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)

R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * p.inertiaDeg' ↑P ≠ 0

Tactic:
exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg'_pos p P.1).ne'

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 < x2) (Iic a)

Tactic:
by
  simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊓ y ∈ carrier

Tactic:
suffices x ⊓ y = sInf {x, y} by exact this ▸ sInfClosed' (fun z hz ↦ by aesop)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊓ y = sInf {x, y}
Module: Mathlib.Order.Completion

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

Tactic:
by
  simpa using ofObject_le_ofAttribute_iff (r := (· ≤ ·)) (a := a)

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
A : Set α
hAs : A ⊆ s
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
⊢ x ∈ s

Tactic:
obtain ⟨f, rfl⟩ := hAc.exists_eq_range hA_ne
    rw [(IsLUB.unique hx isLUB_iSup : x = ⨆ n, f n)]
    exact hs f (by grind)

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

Goal state before:
pp: α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
S : Set (Set α)
h : S.Countable
a : ∀ s ∈ S, s ∈ l
⊢ #↑S < ℵ_ 1

Tactic:
lt_aleph_one_iff,

Goal state after:
α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
S : Set (Set α)
h : S.Countable
a : ∀ s ∈ S, s ∈ l
⊢ #↑S ≤ ℵ₀
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_1
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel ≤ Q.Rel
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
⊢ ∃ y ∈ Q, S ⊆ y

Tactic:
refine ⟨T, hT, fun a haS ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel ≤ Q.Rel
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
a : α
haS : a ∈ S
⊢ a ∈ T
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∉ u
⊢ f (f a) = f a

Tactic:
simp_rw [hf.apply_of_notMem ha]

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

Goal state before:
pp: case pos
α : 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 (f₀ h.choose)

Tactic:
exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h : ¬b ≤ a
⊢ b = if a ≤ b then b else a

Tactic:
rw [if_pos (Std.le_of_lt (Std.not_le.mp h))]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: case mp
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : S.restrictAux a ≤ b
⊢ a ≤ ↑b

pp: case mpr
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ ↑b
⊢ S.restrictAux a ≤ b

Tactic:
· exact le_trans (by simp +contextual [restrictAux]) h

Goal state after:
case mpr
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ ↑b
⊢ S.restrictAux a ≤ b
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))

Tactic:
exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩

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
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
⊢ ∀ᵐ (ω : Ω) ∂μ, Monotone fun x ↦ predictablePart f ℱ μ x ω

Tactic:
filter_upwards [this] with ω h

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
ω : Ω
h : ∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | ↑ℱ i] ω
⊢ Monotone fun x ↦ predictablePart f ℱ μ x ω
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})

Tactic:
rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]

Goal state after:
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 (X m) (n + 1) ⁻¹' {s})
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
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ StronglyMeasurable (f 0)

Tactic:
exact (hf 0).mono (ℱ.mono zero_le)

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

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

Tactic:
obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he

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

Goal state before:
pp: case refine_2.hf
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ StronglyMeasurable μ[f (k + 1) - f k | ↑ℱ k]

Tactic:
exact stronglyMeasurable_condExp.mono (ℱ.mono hk.le)

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 ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ hk₂⟩

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
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
⊢ MeasurableSet {ω | τ ω < ↑i}

pp: case neg
Ω : 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
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
· suffices {ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
    ext1 ω
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
    cases τ ω with
    | top => simp
    | coe t => norm_cast; exact isMin_iff_forall_not_lt.mp hi_min t

Goal state after:
case neg
Ω : 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
⊢ MeasurableSet {ω | τ ω < ↑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
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by
  by_cases hi_min : IsMin i
  · suffices {ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
    ext1 ω
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
    cases τ ω with
    | top => simp
    | coe t => norm_cast; exact isMin_iff_forall_not_lt.mp hi_min t
  obtain ⟨seq, -, -, h_tendsto, h_bound⟩ :
      ∃ seq : ℕ → ι, Monotone seq ∧ (∀ j, seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ j, seq j < i :=
    h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)
  have h_Iio_eq_Union : Set.Iio (i : WithTop ι) = ⋃ j, {k : WithTop ι | k ≤ seq j} := by
    ext1 k
    push _ ∈ _
    refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
    · rw [tendsto_atTop'] at h_tendsto
      cases k with
      | top => simp at hk_lt_i
      | coe k =>
        norm_cast at hk_lt_i ⊢
        have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
        obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
        exact ⟨a, ha a le_rfl⟩
    · obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
      exact hk_seq_j.trans_lt (mod_cast h_bound j)
  have h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i := by
    ext1 ω; push _ ∈ _; rfl
  rw [h_lt_eq_preimage, h_Iio_eq_Union]
  simp only [Set.preimage_iUnion, Set.preimage_ofPred_eq]
  exact MeasurableSet.iUnion fun n => f.mono (h_bound n).le _ (hτ.measurableSet_le (seq n))

Goal state after: