mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ p.inertiaDeg' P ≤
    p.ramificationIdx' P * p.inertiaDeg' P +
      ∑ x ∈ (IsDedekindDomain.primesOverFinset p S).erase P, p.ramificationIdx' x * p.inertiaDeg' x

Tactic:
refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _)

Goal state after:
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ 0 < p.ramificationIdx' P
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ i ∈ c, f i = g i
⊢ f (ωSup c) = g (ωSup c)

Tactic:
by
    rw [f.continuous, g.continuous]
    congr 1
    ext x
    apply hc _ ⟨_, rfl⟩

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
p : ℕ
hp : Nat.Prime p
⊢ A ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ A ↑⟨p, hp⟩ =ᵐ[μ] univ

Tactic:
let f : 𝕊 → 𝕊 := fun y => (p : ℕ) • y

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
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y ↦ p • y
⊢ A ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ A ↑⟨p, hp⟩ =ᵐ[μ] univ
Module: Mathlib.Order.CompleteSublattice

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

Tactic:
coe_sInf',

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

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ t

Tactic:
rw [← h.eq]
  exact upperPolar_lowerPolar_monotone r ht'

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
⊢ A ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a} →
    A.Nonempty →
      A.Countable → ∀ (x : α), IsLUB A x → x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}

Tactic:
hA

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA : A ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
⊢ A.Nonempty →
    A.Countable → ∀ (x : α), IsLUB A x → x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
⊢ a ∈ countableSupClosure s ↔ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a

Tactic:
by
  suffices countableSupClosure s = {a | ∃ (t : ℕ → α), (∀ n, t n ∈ s) ∧ ⨆ n, t n = a} by simp [this]
  have h_csc : CountableSupClosed {a | ∃ (t : ℕ → α), (∀ n, t n ∈ s) ∧ ⨆ n, t n = a} := by
    refine .of_iSup_mem fun A hA ↦ ?_
    choose B hB hB_eq using hA
    refine ⟨fun n ↦ B (Nat.unpair n).1 (Nat.unpair n).2, fun _ ↦ hB _ _, ?_⟩
    simp [iSup_unpair, ← hB_eq]
  refine le_antisymm (countableSupClosure_min ?_ h_csc) ?_
  · exact fun a ha ↦ ⟨fun _ ↦ a, by simp [ha]⟩
  · rintro _ ⟨u, hus, rfl⟩
    exact countableSupClosed_countableSupClosure.iSup_mem fun n ↦ subset_countableSupClosure (hus n)

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioc a b).ncard = b - a

Tactic:
by
  simpa [← Set.ncard_coe_finset] using Nat.card_Ioc a b

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ MonovaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ MonotoneOn g s

Tactic:
refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ f i ≤ f j

case refine_2
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ g i ≤ g j

case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
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 α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have J₁S : ↑J₁ ∉ S := fun h => J₁J (hmax.eq_of_le h (le_sup_left : J ≤ J₁)).symm

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ MeasurableSet {ω | (n + 1, ω) ∈ s}

Tactic:
rw [(by aesop : {ω | (n + 1, ω) ∈ s} = (Prod.mk (α := Set.singleton (n + 1)) (β := Ω)
      ⟨n + 1, rfl⟩) ⁻¹' ((fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' s))]
  refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
    measurable_prodMk_left <| measurableSet_preimage ?_ hs
  rw [measurable_iff_comap_le, MeasurableSpace.comap_le_iff_le_map]
  refine MeasurableSpace.generateFrom_le ?_
  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
  · rw [MeasurableSpace.map_def,
      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
    · simp
    · ext p
      simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
        Set.mem_empty_iff_false, iff_false, not_and]
      exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)
  · rw [MeasurableSpace.map_def]
    obtain hni | hin := lt_or_ge n i
    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
      · simp
      · ext p
        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
          iff_false, not_and]
        rw [p.1.2]
        grind
    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
          = {⟨n + 1, rfl⟩} ×ˢ A)]
      · exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
      · ext p
        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
          and_congr_left_iff]
        intro hp2
        rw [p.1.2]
        exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : PartialOrder F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
ω : Ω
hω : μ[c • f j | ↑ℱ i] ω = (c • μ[f j | ↑ℱ i]) ω
hle : μ[f j | ↑ℱ i] ω ≤ f i ω
⊢ μ[(c • f) j | ↑ℱ i] ω ≤ (c • f) i ω

Tactic:
simpa only [hω, Pi.smul_apply] using smul_le_smul_of_nonneg_left hle hc

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ hittingAfter u Set.univ n ω = ↑n

Tactic:
classical
  simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici

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

Tactic:
by
  classical
  rw [hittingBtwn, ite_eq_right_iff]

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 τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i < τ ω} ↔ ω ∈ {ω | τ ω ≤ ↑i}ᶜ

Tactic:
simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, not_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 ι
hl : ∃ x, ∃ (_ : n ≤ x), u x ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hl

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
j : ι
hj₁ : n ≤ j
hj₂ : u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ 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₂ ω
⊢ 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) ?_)

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₂ ω
⊢ (upcrossingsBefore a b f N ω).succ ∈ {n | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1}
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
hτbdd : τ x ≤ ↑N
h : τ x = ⊤
⊢ False

Tactic:
by simp [h] at hτbdd

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
hτbdd : τ x ≤ ↑N
m : ι
hm : n < m
hτ : τ x = ↑m
h : τ x = ⊤
⊢ False

Tactic:
by simp [h] at hτbdd

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ 0 ≤ ∫ (a : Ω), (fun ω ↦ (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (f (i + 1) - f i)) ω) a ∂μ

Tactic:
simp only [Finset.sum_apply]
    have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} := by
      intro i
      refine (hτ i).inter ?_
      convert! (hπ i).compl using 1
      ext x
      simp; rfl
    rw [integral_finsetSum]
    · refine Finset.sum_nonneg fun i _ => ?_
      rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
      · exact hf.setIntegral_le (Nat.le_succ i) (this _)
      · exact (hf.integrable _).integrableOn
      · exact (hf.integrable _).integrableOn
    intro i _
    exact Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _))
      (𝒢.le _ _ (this _))

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

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s → MeasurableSet s

Tactic:
change MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s →
      MeasurableSet[(hτ.min hπ).measurableSpace] s

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ∧ MeasurableSet s → MeasurableSet s
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 : ι
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i

Tactic:
rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]

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

Goal state before:
pp: case compl
Ω : 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 Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω), g x ∂μ - ∫ (x : Ω) in t, g x ∂μ =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ - ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ

Tactic:
← setIntegral_univ,

Goal state after:
case compl
Ω : 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 Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω) in Set.univ, g x ∂μ - ∫ (x : Ω) in t, g x ∂μ =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ - ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u : Ω → E
⊢ ∀ ⦃g : Ω → E⦄,
    Disjoint (Function.support u) (Function.support g) →
      MemLp u 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable u →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (u + g) x ∂μ = ∫ (x : Ω) in s, (u + g) x ∂μ

Tactic:
v

Goal state after:
case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
⊢ Disjoint (Function.support u) (Function.support v) →
    MemLp u 1 μ →
      MemLp v 1 μ →
        StronglyMeasurable u →
          StronglyMeasurable v →
            μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ →
              μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ →
                μ.real s • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u : Ω → E
⊢ ∀ ⦃g : Ω → E⦄,
    u =ᵐ[μ] g →
      MemLp u 1 μ →
        μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
v

Goal state after:
case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
⊢ u =ᵐ[μ] v →
    MemLp u 1 μ →
      μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ → μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ f n ω)
n : ℕ
⊢ f n ω + -f 0 ω ≤ b + |f 0 ω|

Tactic:
exact add_le_add (hb ⟨n, rfl⟩) (neg_le_abs _)

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

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ i ∈ ∅, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
simp only [Finset.sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _

Goal state after: