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

Goal state before:
pp: case f
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
x : Fin n
| A.det • a' x • a x

Tactic:
rw [smul_comm A.det, d_smul, smul_zero]

Goal state after:
case f
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
x : Fin n
| 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: 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
⊢ Irreducible (⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne)

Tactic:
set πᵥ := degree_lt_wf.min _ hne
  have hπᵥ : v πᵥ < 1 ∧ πᵥ ≠ 0 := degree_lt_wf.min_mem _ hne
  refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩
  · simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]
    intro ⟨a, ha0, ha⟩
    rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ
    grind
  · by_contra! H
    simp only [hab, ne_eq, mul_eq_zero, not_or] at hπᵥ
    have hva := one_le_valuation_factor hne hπᵥ hab H.2
    simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab
    have := Right.one_le_mul (one_le_valuation_factor hne hπᵥ hab H.1) hva
    simp only [coePolynomial_eq_algebraMap, map_mul] at hπᵥ this
    grind

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
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
⊢ False

Tactic:
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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (k + 1)!) + ↑(m ^ k !) * 1 * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
· norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]

Goal state after:
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
Module: Mathlib.NumberTheory.Wilson

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

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

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

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

Tactic:
· intro a ha
    rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]
    constructor
    · apply Nat.pos_of_ne_zero; rw [← @val_zero p]
      intro h; apply Units.ne_zero a (val_injective p h)
    · exact val_lt _

Goal state after:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, (↑a₁).val = (↑a₂).val → a₁ = a₂

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

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedGT ι
x✝ : Set (Colex ((i : ι) → α i))
⊢ IsLUB x✝ (sSup x✝)

Tactic:
by exact Lex.isLUB_sSup (ι := ιᵒᵈ)

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ principal a < c ↔ ∃ b ∈ c.left, a < b

Tactic:
by
  rw [← not_le, le_principal_iff]
  rw [not_iff_comm, not_exists, ← le_principal_iff]
  simp_rw [← not_le, not_and, not_not]
  rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
x : α
s : Set α
hs_subset : s ⊆ {x}
hs_ne : s.Nonempty
x✝ : s.Countable
y : α
hy : IsLUB s y
h_eq : s = {x}
⊢ y ∈ {x}

Tactic:
simp_all only [subset_refl, singleton_nonempty, countable_singleton, mem_singleton_iff]

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
x : α
s : Set α
y : α
hy : IsLUB {x} y
h_eq : s = {x}
⊢ y = x
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: case mp
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

pp: case mpr
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t

Tactic:
· rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
      exact ⟨v, vsets, (SetRel.preimage_mono hv).trans h⟩

Goal state after:
case mpr
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)

Tactic:
by
  apply NormedAddCommGroup.exists_norm_nsmul_le (μ := volume) ξ hn
  rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊔ z

Tactic:
simpa [inf_assoc] using inf_le_of_right_le inf_le_sup

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
⊢ IsLUB ((fun a ↦ Prod.map f g (a, b)) '' d) ((fun a ↦ Prod.map f g (a, b)) c)

Tactic:
· have e2 : ((fun a ↦ (f a, g b)) '' d) = (f '' d) ×ˢ {g b} := by aesop
    simp_rw [Prod.map_apply, e2]
    exact .prod (hd₁.image _) (singleton_nonempty _) (hf hd₁ hd₂ hdc) isLUB_singleton

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: case pos
α : 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 : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : a = b
⊢ compare a b = Ordering.eq

pp: case neg
α : 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 : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ compare a b = Ordering.gt

Tactic:
case _ => rwa [Std.compare_eq_iff_eq]

Goal state after:
case neg
α : 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 : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ compare a b = Ordering.gt
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ¬v₁ ⊓ v₂ = ⊥
⊢ t₁ = t₂

Tactic:
← ne_eq,

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : v₁ ⊓ v₂ ≠ ⊥
⊢ t₁ = t₂
Module: Mathlib.Order.Sublocale

Goal state before:
pp: 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
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ Subtype.val '' {s | x ≤ ↑s} ⊆ ↑S

Tactic:
simp +contextual [Set.subset_def]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
⊢ Adapted f u

Tactic:
intro i
  have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
  rw [this]
  exact (h i).comp measurable_prodMk_left

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)

Tactic:
ext m
    simp only [Set.mem_singleton_iff, Set.mem_Ioc]
    lia

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m_1 x ↦ (StronglyMeasurable.approx h𝓕 m_1) (↑x.1, x.2)
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2

Tactic:
refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_2
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m✝
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m x ↦ (StronglyMeasurable.approx h𝓕 m) (↑x.1, x.2)
m : ℕ
⊢ ∀ (x : E), MeasurableSet (X m ⁻¹' {x})

case refine_2
Ω : Type u_1
ι : Type u_2
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m✝
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m x ↦ (StronglyMeasurable.approx h𝓕 m) (↑x.1, x.2)
m : ℕ
⊢ (Set.range (X m)).Finite

case refine_3
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m_1 x ↦ (StronglyMeasurable.approx h𝓕 m_1) (↑x.1, x.2)
⊢ ∀ (x : { x // x ∈ Set.Iic i } × Ω),
    Tendsto (fun n ↦ ((fun m_1 ↦ { toFun := X m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n) x) atTop
      (𝓝 ((fun p ↦ u (↑p.1) p.2) x))
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

Tactic:
refine EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le

Goal state after:
case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j | ↑ℱ i] - μ[f i | ↑ℱ i]
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
⊢ hittingBtwn u Set.univ n m = fun x ↦ min n m

Tactic:
by
  ext ω
  simp only [hittingBtwn_def, Set.mem_Icc, Set.mem_univ, and_true, Set.ofPred_true, Set.inter_univ]
  by_cases hnm : n ≤ m <;> simp [hnm] <;> grind

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 k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ k

Tactic:
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩

Goal state after:
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 : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
⊢ MeasurableSet (⋃ (_ : j < ↑i), {ω | τ ω ≤ j})

Tactic:
Set.iUnion_eq_if

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 : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
⊢ MeasurableSet (if j < ↑i then {ω | τ ω ≤ j} else ∅)
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]

Goal state after:
case succ
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N k ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N k ω)
this : IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N (k + 1) ω)
Module: Mathlib.Probability.Process.HittingTime

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

Tactic:
simp_rw [hittingBtwn, if_neg h_exists]

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ upcrossingStrat a b f N n ω ≤ 1

Tactic:
by
  rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]
  · exact Set.indicator_le_self' (fun _ _ => zero_le_one) _
  intro i _ j _ hij
  simp only [Set.Ico_disjoint_Ico]
  obtain hij' | hij' := lt_or_gt_of_ne hij
  · rw [min_eq_left (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_right (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
    refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))
  · rw [min_eq_right (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_left (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
    refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ≤ fun x ↦ ↑j

Tactic:
intro ω
    simp only [Set.piecewise, ENat.some_eq_natCast]
    split_ifs with hω
    · exact mod_cast hij
    · norm_cast

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (fun ω ↦ rexp (t * X ω)) μ
hν : Integrable (fun ω ↦ rexp (t * X ω)) ν
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t

Tactic:
by
  rw [mgf, integral_add_measure hμ hν, mgf, mgf]

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

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z ↦
    ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (fun z ↦ ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

Goal state after: