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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
⊢ Filter.Tendsto (⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))) (nhds 0) (nhds 0)

Tactic:
(IsValuativeTopology.hasBasis_nhds_zero _).tendsto_iff
    (IsValuativeTopology.hasBasis_nhds_zero _)

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
⊢ ∀ (ib : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ),
    True →
      ∃ ia,
        True ∧
          ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
            (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
              {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑ib}
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : Nat.Prime p ∧ p ∣ d
⊢ s.nu p < 1

Tactic:
apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2

Tactic:
by
        rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _] <;>
          simpa [sq, parity_simps, ← even_iff_two_dvd]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : Nat.Prime p
⊢ 0 < 1 - s.nu p

Tactic:
have hp_dvd : p ∣ s.prodPrimes := (Nat.dvd_of_mem_primeFactors hp).trans hl

Goal state after:
s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : Nat.Prime p
hp_dvd : p ∣ s.prodPrimes
⊢ 0 < 1 - s.nu p
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
⊢ p % 4 ≠ 3

Tactic:
by
  obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd (Nat.dvd_of_mem_primeFactors hp) hs
  rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h
  have : Fact p.Prime := ⟨Nat.prime_of_mem_primeFactors hp⟩
  exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

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

Tactic:
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)

Goal state after:
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
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
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
hx' : x ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x, hx✝⟩

Tactic:
obtain ⟨y', hy', z, hz, rfl⟩ := Submodule.mem_sup.mp hx'

Goal state after:
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
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
y' : S
hy' : y' ∈ span {a}
z : S
hz : z ∈ P ^ (i + 1)
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : y' + z ∈ P ^ i
hx' : y' + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z), hx✝⟩
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fa : eval α (map (algebraMap ℤ ℝ) f) = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

Tactic:
set fR : ℝ[X] := map (algebraMap ℤ ℝ) f

Goal state after:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
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)
⊢ Q j

Tactic:
dsimp only [Q]

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)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ j)) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2
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)
⊢ Q e

Tactic:
dsimp only [Q]

Goal state after:
case refine_2
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)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ e)) = (e - e) • Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ ∑ i ∈ {0}, 1 / ↑m ^ i ! = ↑1 / ↑(m ^ 0!)

Tactic:
sum_singleton,

Goal state after:
m : ℕ
hm : 0 < m
⊢ 1 / ↑m ^ 0! = ↑1 / ↑(m ^ 0!)
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: ⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → o.Nonempty → (o ∩ {x | Irrational x}).Nonempty

Tactic:
rintro _ a b hlt rfl _

Goal state after:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ (Ioo ↑a ↑b ∩ {x | Irrational x}).Nonempty
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

Tactic:
Rat.cast_inv,

Goal state after:
case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * (↑r)⁻¹ = ↑1
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
← sInter_range _

Goal state after:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l
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 b : α
⊢ SurjOn f (Ioo a b) (Ioo (f a) (f b))

Tactic:
by
  intro p hp
  rcases h_surj p with ⟨x, rfl⟩
  refine ⟨x, mem_Ioo.2 ?_, rfl⟩
  contrapose! hp
  exact fun h => h.2.not_ge (h_mono <| hp <| h_mono.reflect_lt h.1)

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

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
hp : f a ∈ Ico (f a) (f b)
⊢ f a ∈ f '' Ico a b

pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ico a b

Tactic:
· exact mem_image_of_mem f (left_mem_Ico.mpr hab)

Goal state after:
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ico a b
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
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (y ⊓ (x ⊓ z)) (y ⊓ z)

Tactic:
simpa [inf_comm x, ← inf_inf_distrib_left] using this

Goal state after:
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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
⊢ i ≠ j

Tactic:
by rintro rfl; simp [← h2, π_refl] at hne

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
rw [le_iInf₂_iff]

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : ↑(Prod.fst '' d)
⊢ IsLUB (f '' {↑a} ×ˢ (Prod.snd '' d)) (?m.129 a)

Tactic:
singleton_prod,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : ↑(Prod.fst '' d)
⊢ IsLUB (f '' Prod.mk ↑a '' Prod.snd '' d) (?m.129 a)
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
a : α
haS : a ∈ S
T' : Set α
hT' : T' ∈ Q
haT' : a ∈ T'
hxT' : x ∈ T'
⊢ a ∈ T

Tactic:
exact eq_of_mem_of_mem hT hT' hxT hxT' ▸ haT'

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.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

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
c : ℝ
n : ℕ
⊢ predictablePart (c • f) ℱ μ n =ᵐ[μ] c • predictablePart f ℱ μ n

Tactic:
simp only [predictablePart, Finset.smul_sum]

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
c : ℝ
n : ℕ
⊢ ∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | ↑ℱ i] =ᵐ[μ] ∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | ↑ℱ x]
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 ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
h_exists_k_le_seq : ∃ i, k ≤ ↑(seq i)
⊢ k < ↑i

Tactic:
· obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
      exact hk_seq_j.trans_lt (mod_cast h_bound j)

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

Goal state before:
pp: case neg
Ω : 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₂ ω
hN : N = 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']

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

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
⊢ upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1) ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = lowerCrossingTime a b f N (k + 1)

Tactic:
have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
        upperCrossingTime a b f N (k + 1) := by
      ext ω
      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
      split_ifs with h₁ h₂ h₂
      · simp_rw [← sub_le_iff_le_add, hf ω]
      · refine False.elim (h₂ ?_)
        simp_all only [Set.mem_Ici, not_true_eq_false]
      · refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]
      · rfl
    refine ⟨this, ?_⟩
    ext ω
    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
    split_ifs with h₁ h₂ h₂
    · simp_rw [hf' ω]
    · refine False.elim (h₂ ?_)
      simp_all only [Set.mem_Iic, not_true_eq_false]
    · refine False.elim (h₁ ?_)
      simp_all only [Set.mem_Iic]
    · rfl

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
constructor <;> rintro ⟨k, hk⟩

Goal state after:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
by
  suffices Indep (⨆ k ∈ ({j} : Set ι), MeasurableSpace.comap (f k) mβ)
      (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ by rwa [iSup_singleton] at this
  exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
⊢ IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA

Tactic:
refine fun i ↦ (Measurable.untopA ?_).stronglyMeasurable
  let m_prod : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (f i)
  let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
    @Subtype.instMeasurableSpace (Set.Iic i × Ω) _ m_prod
  let s := {p : Set.Iic i × Ω | τ p.2 ≤ i}
  have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)
  have h_meas_fst : ∀ t : Set (Set.Iic i × Ω),
      Measurable[m_set t] fun x : t => ((x : Set.Iic i × Ω).fst : ι) :=
    fun t => (@measurable_subtype_coe (Set.Iic i × Ω) m_prod _).fst.subtype_val
  refine measurable_of_restrict_of_restrict_compl hs ?_ ?_
  · refine Measurable.min (h_meas_fst s).withTop_coe ?_
    refine measurable_of_Iic fun j ↦ ?_
    cases j with
    | top => simp
    | coe j =>
      have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_ofPred_eq, Set.mem_ofPred_eq, iff_and_self]
        exact fun _ => ω.prop
      rw [h_set_eq]
      suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
      exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)
  · let sc := sᶜ
    suffices h_min_eq_left :
      (fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
        ↑(x : Set.Iic i × Ω).fst by
      simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]
      exact (h_meas_fst _).withTop_coe
    ext1 ω
    rw [min_eq_left]
    have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.prop
    by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤
    · simp [h]
    · lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht
      norm_cast
      refine hx_fst_le.trans (le_of_lt ?_)
      convert! ω.prop
      simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_ofPred_eq, ← ht]
      norm_cast

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * (α * X x)) ∂μ = ∫ (x : Ω), rexp (α * t * X x) ∂μ

Tactic:
mul_comm α t,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * (α * X x)) ∂μ = ∫ (x : Ω), rexp (t * α * X x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
⊢ (fun ω ↦ rexp (s * X ω)) ⟂ᵢ[μ] fun ω ↦ rexp (t * Y ω)

Tactic:
by
  have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp
  change IndepFun ((fun x => exp (s * x)) ∘ X) ((fun x => exp (t * x)) ∘ Y) μ
  exact IndepFun.comp h_indep (h_meas s) (h_meas t)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : ↑t = τ ω
hbdd : t ≤ N
⊢ ↑t ∈ WithTop.some '' ↑(Finset.range (N + 1))

Tactic:
simp only [ENat.some_eq_natCast, Finset.coe_range]

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
N : ℕ
ω : Ω
t : ℕ
ht : ↑t = τ ω
hbdd : t ≤ N
⊢ ↑t ∈ (fun a ↦ ↑a) '' Set.Iio (N + 1)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ X ω ^ p) μ

Tactic:
have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
  · simpa using h
  · simpa using ht_int_pos
  · simpa using ht_int_neg

Goal state after: