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

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (a * b).x

Tactic:
simp only [x_mul]
  refine neg_lt_iff_pos_add'.mp (abs_lt.mp ?_).1
  rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ←
    sub_pos]
  ring_nf
  rcases le_or_gt 0 d with h | h
  · positivity
  · rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']
    simp

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
⊢ T_gen p F a < 1

Tactic:
have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm

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
h : ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2

Tactic:
a.prop_x,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - (1 + d * a.y ^ 2)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x ^ 2 * a₁.y ^ 2 ≤ a.y ^ 2 * a₁.x ^ 2

Tactic:
a.prop_x,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ (1 + d * a.y ^ 2) * a₁.y ^ 2 ≤ a.y ^ 2 * a₁.x ^ 2
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a : K
hπᵥ : v ((algebraMap K[X] K⟮X⟯) (Polynomial.C a)) < 1 ∧ Polynomial.C a ≠ 0
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False

Tactic:
algebraMap_C,

Goal state after:
case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a : K
hπᵥ : v (C a) < 1 ∧ Polynomial.C a ≠ 0
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
⊢ s.nu d < 1

Tactic:
have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
  have := hd_sq.ne_zero
  calc
    s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
    _ < ∏ p ∈ d.primeFactors, 1 := by
      apply prod_lt_prod_of_nonempty
      · intro p hp
        simp only [mem_primeFactors] at hp
        apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
      · intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
      · simp only [nonempty_primeFactors, show 1 < d by lia]
    _ = 1 := by
      simp

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_3
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

Tactic:
exact lt_of_le_of_ne hp.1.two_le (hodd.ne_two_of_dvd_nat (dvd_refl _)).symm

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x • Quotient.mk'' y) =
    (RingHom.id (R ⧸ p)) (Quotient.mk'' x) • p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)

Tactic:
simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply,
      quotientToQuotientRangePowQuotSuccAux_mk]

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    X ^ (p - 1) * f ^ p = (X - C r) ^ (p - 1) * p' →
      eval r (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval r p' + p ! • eval r gp'
⊢ X ^ (p - 1) * f ^ p = (X - C 0) ^ (p - 1) * ?m.190

Tactic:
by rw [C_0, sub_zero]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = -1

Tactic:
refine
    calc
      ((p - 1)! : ZMod p) = ∏ x ∈ Ico 1 (succ (p - 1)), (x : ZMod p) := by
        rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
      _ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := ?_
      _ = -1 := by
        simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x, ↑x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

pp: case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0

Tactic:
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]

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
x : ℕ
⊢ (c.map ↑f) x = (c.map ↑g) x

Tactic:
apply hc _ ⟨_, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
rintro ⟨m, hm₁, hm₂, hx⟩; exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ x✝ ≤ sInf A.right ↔ x✝ ∈ A.left

Tactic:
le_sInf_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.right, x✝ ≤ b) ↔ x✝ ∈ A.left
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b a) → a = b

Tactic:
rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩

Goal state after:
case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
rw [rtendsto_def]
  simp_rw [← l₂.mem_sets]
  constructor
  · simpa [Filter.le_def, rcomap, SetRel.mem_image]
      using fun h s t tl₂ => mem_of_superset (h t tl₂)
  · simpa [Filter.le_def, rcomap, SetRel.mem_image]
      using fun h t tl₂ => h _ t tl₂ Set.Subset.rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁

Tactic:
intro h' s sl₂

Goal state after:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.preimage s ∈ l₁
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ

Tactic:
· obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hj)
    grind [insertNth_apply_same, insertNth_apply_above, hf j.castSucc_le_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))

Tactic:
← compl_compl (Ioi (f a))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))

Tactic:
← Ioi_union_left,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ici (f a))
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
⊢ ∀ (a b : αs), a ≤ b ∧ a ≠ b → ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
hcovby

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
⊢ ∀ (a b : αs), a ≤ b ∧ a ≠ b → ∃ x, (a ≤ x ∧ a.fst + 1 = x.fst) ∧ x ≤ b
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.I)ᶜ

Tactic:
rw [IF.compl_I_eq_F]

Goal state after:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter ↑IF.F
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
· apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
· apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
· rw [← h.2]
      apply iInf₂_mono
      intro x _
      apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

Tactic:
rw [← h.2]
      apply le_trans (le_rfl) (le_iSup₂ b hb)

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := ⋯
this : MeasurableSpace Ω := ⋯
X : ℕ → Ω → E := ⋯
m : ℕ
s : E
⊢ MeasurableSet (⇑(StronglyMeasurable.approx h𝓕 m) ⁻¹' {s})

Tactic:
apply (h𝓕.approx m).measurableSet_fiber

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 ℱ μ
⊢ Supermartingale (c • f) ℱ μ

Tactic:
by
  refine ⟨hf.1.smul c, fun i j hij => ?_, fun i => (hf.2.2 i).smul c⟩
  filter_upwards [condExp_smul c (f j) (ℱ i), hf.2.1 i j hij] with ω hω hle
  simpa only [hω, Pi.smul_apply] using smul_le_smul_of_nonneg_left hle hc

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 ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (f i)

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
hji : ¬j < ↑i
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (f i)

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 ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (f i)

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
n : ℕ
s : Set Ω
ms : MeasurableSet s
hs : (μ.trim ⋯) s < ∞
⊢ ∫ (x : Ω) in s, f n x ∂μ.trim ⋯ = ∫ (x : Ω) in s, μ[f (n + 1) | ↑𝒢 n] x ∂μ.trim ⋯

Tactic:
← setIntegral_trim (𝒢.le n) (hadp n) ms,

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✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
n : ℕ
s : Set Ω
ms : MeasurableSet s
hs : (μ.trim ⋯) s < ∞
⊢ ∫ (x : Ω) in s, f n x ∂μ = ∫ (x : Ω) in s, μ[f (n + 1) | ↑𝒢 n] x ∂μ.trim ⋯
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
have := (crossing_eq_crossing_of_lowerCrossingTime_lt hNM
    (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
ω : ι
⊢ ω ∈ {i ∈ s | y ∈ {ω | τ ω = ↑i}} ↔ ω ∈ {(τ y).untopA}

Tactic:
simp only [Set.mem_ofPred_eq, Finset.mem_filter, Finset.mem_singleton]

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = ↑ω ↔ ω = (τ y).untopA
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ μ.real {ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ

Tactic:
by
      have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
      rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
by
  refine (measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_
  rw [exp_add]
  exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
by
  simp_rw [← memLp_one_iff_integrable] at hu ⊢
  exact memLp_stoppedProcess_of_mem_finset hτ hu n hbdd

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

Goal state before:
pp: case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [abs_of_nonpos ht_neg.le, sup_comm]
    convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])
    simp

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

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + (u - v) = u

Tactic:
by abel

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

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l = v - (v - l)

Tactic:
by abel

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (⇑L) p μ

Tactic:
suffices MemLp (id ∘ L) p μ from this
  rw [← memLp_map_measure_iff (by fun_prop) (by fun_prop), IsGaussian.map_eq_gaussianReal L]
  convert! memLp_id_gaussianReal p.toNNReal
  simp [hp]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ((covarianceBilin (Measure.map (fun x ↦ c + x) μ)) x✝¹) x✝ = ((covarianceBilin μ) x✝¹) x✝

Tactic:
rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]

Goal state after:
case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
refine this.trans_eq ?_
    simp only [ENNReal.toReal_mul]
    rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity),
      ← Real.rpow_mul (by positivity), mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top, ENNReal.toReal_rpow]
    simp

Goal state after: