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

Goal state before:
pp: A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
⊢ v.intValuation x ^ v.asIdeal.ramificationIdx' w.asIdeal = w.intValuation ((algebraMap A B) x)

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [ramificationIdx'_ne_zero_of_liesOver w.asIdeal v.ne_bot]
  rw [intValuation_eq_exp_neg_multiplicity v hx, intValuation_eq_exp_neg_multiplicity w (by simpa),
    ← Set.image_singleton, ← Ideal.map_span, exp_neg, exp_neg, inv_pow, ← exp_nsmul,
    Int.nsmul_eq_mul, inv_inj, exp_inj, ← Nat.cast_mul, Nat.cast_inj]
  refine multiplicity_eq_of_emultiplicity_eq_some ?_ |>.symm
  replace hx : Ideal.span {x} ≠ ⊥ := by simp [hx]
  rw [emultiplicity_map_eq_ramificationIdx'_mul hx v.irreducible w.irreducible w.ne_bot,
    Nat.cast_mul, (FiniteMultiplicity.of_prime_left v.prime hx).emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
j : ℤ
h : r > 0
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
cases le_or_gt (⌊(j + 1) / r⌋ * r) j

Goal state after:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j < ↑⌊(↑j + 1) / r⌋ * r
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
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✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ ∃ z, v f = v ↑πᵥ ^ z

Tactic:
have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle
  induction f using RatFunc.induction_on with
  | f p q hq =>
    use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors -
      (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors
    simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle
        (p := p) (by aesop)]

Goal state after:
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✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ ∃ z, v f = v ↑πᵥ ^ z

Tactic:
by
  have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle
  induction f using RatFunc.induction_on with
  | f p q hq =>
    use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors -
      (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors
    simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle
        (p := p) (by aesop)]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
⊢ (s.nu (d * e))⁻¹ * (↑(μ (d, e).1) * s.nu (d, e).1) = ↑(μ (d, e).1) * (s.nu (d, e).2)⁻¹

Tactic:
obtain ⟨hde, -⟩ : d.Coprime e ∧ _ := by simpa only [squarefree_mul_iff] using hl

Goal state after:
case a
s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
hde : d.Coprime e
⊢ (s.nu (d * e))⁻¹ * (↑(μ (d, e).1) * s.nu (d, e).1) = ↑(μ (d, e).1) * (s.nu (d, e).2)⁻¹
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
have := Fact.mk hp

Goal state after:
p : ℕ
hp : Prime p
this : Fact (Prime p)
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

pp: case inr
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
· use a, b, c, d; simpa using habcd

Goal state after:
case inr
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.mk
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 : span {a} ≤ P ^ i
a_notMem : ¬span {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
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
have hspan0 : span {a} ≠ ⊥ := fun ha ↦ a_notMem (ha ▸ bot_le)

Goal state after:
case mk.mk
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 : span {a} ≤ P ^ i
a_notMem : ¬span {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
hspan0 : span {a} ≠ ⊥
⊢ x ∈ span {a} ⊔ P ^ (i + 1)
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)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ e)) = 0 • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
zero_nsmul,

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)) = 0
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ ({x | Irrational x} ∩ Ioo ↑a ↑b).Nonempty

Tactic:
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)

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

Goal state before:
pp: p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)

Tactic:
exact h.mul_nat hn

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

Goal state before:
pp: ⊢ {x | ∃ p > 2, LiouvilleWith p x} ⊆
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Tactic:
by
  rintro x ⟨p, hp, hxp⟩
  rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
  rw [lt_sub_iff_add_lt'] at hn
  suffices ∀ y : ℝ, LiouvilleWith p y → y ∈ Ico (0 : ℝ) 1 → ∃ᶠ b : ℕ in atTop,
      ∃ a ∈ Finset.Icc (0 : ℤ) b, |y - a / b| < 1 / (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) by
    simp only [mem_iUnion, mem_preimage]
    have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
      simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff,
        mem_Ico, Int.cast_neg, le_add_neg_iff_add_le]
    exact ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
  clear hxp x; intro x hxp hx01
  refine ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono ?_
  rintro b ⟨⟨a, -, hlt⟩, hb⟩
  rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt
  refine ⟨a, ?_, hlt⟩
  replace hb : (1 : ℝ) ≤ b := Nat.one_le_cast.2 hb
  have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
  replace hlt : |x - a / b| < 1 / b := by
    refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)
    calc
      (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
      _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) :=
        rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
    simpa using n.cast_add_one_pos.le
  rw [sub_div' hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_iff_of_pos_right hb0, abs_sub_lt_iff,
    sub_lt_iff_lt_add, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt
  rw [Finset.mem_Icc, ← Int.lt_add_one_iff, ← Int.lt_add_one_iff, ← neg_lt_iff_pos_add, add_comm, ←
    @Int.cast_lt ℝ, ← @Int.cast_lt ℝ]
  push_cast
  refine ⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩
  · simp only [mul_nonneg hx01.left b.cast_nonneg, neg_le_sub_iff_le_add, le_add_iff_nonneg_left]
  · rw [add_le_add_iff_left]
    exact mul_le_of_le_one_left hb0.le hx01.2.le

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

Goal state before:
pp: X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ : s.pt ⟶ (equalizer f g).pt
hm : m✝ ≫ (equalizer f g).ι = s.ι
x : s.pt.carrier
⊢ (ConcreteCategory.hom m✝) x =
    (ConcreteCategory.hom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ }) x

Tactic:
apply Subtype.ext ?_

Goal state after:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ : s.pt ⟶ (equalizer f g).pt
hm : m✝ ≫ (equalizer f g).ι = s.ι
x : s.pt.carrier
⊢ ↑((ConcreteCategory.hom m✝) x) =
    ↑((ConcreteCategory.hom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ }) x)
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ ⨆ n, A n ∈ s

Tactic:
exact hs.isLUB_mem (range A) (by simp [range]; grind) ⟨A i₀, by simp⟩ (countable_range A) _
    isLUB_iSup

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

Goal state before:
pp: a b : ℕ
⊢ (uIcc a b).ncard = (↑b - ↑a).natAbs + 1

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

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

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ y ≈ x ⊔ y

Tactic:
by simpa using c.sup (c.symm h) (c.refl y)

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
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
have : IsStronglyAtomic αs := by
    simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨⟨hij : i ≤ j, h2 : π hij b = a⟩, hne⟩
    have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)
    exact ⟨⟨_, π hle b⟩, ⟨⟨by simp, by rw [π_trans, ← h2]⟩, by simp⟩, ⟨hle, by simp⟩⟩

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
this : IsStronglyAtomic αs
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ I.IsMaximal

Tactic:
simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ ↑J
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ I.IsMaximal

Tactic:
simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
  intro J hIJ x
  rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
  suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
  exact
    sup_mem (J.lower inf_le_right hyJ)
      (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)

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

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Set α
indep : _root_.sSupIndep P
hsSup : sSup P = s
⊢ sSup (P \ {⊥}) = s

Tactic:
by simp [← hsSup]

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

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
⊢ ∃! y, y ∈ Q ∧ x ≤ y

Tactic:
obtain ⟨y, hy, hxy⟩ := h hx

Goal state after:
α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ ∃! y, y ∈ Q ∧ x ≤ y
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
⊢ ∃ y ∈ Q, S ⊆ y

Tactic:
obtain ⟨x, hxS⟩ := nonempty_of_mem hS
    obtain ⟨T, hT, hxT, -⟩ := h x x ⟨S, hS, hxS, hxS⟩
    refine ⟨T, hT, fun a haS ↦ ?_⟩
    obtain ⟨T', hT', haT', hxT'⟩ := h a x ⟨S, hS, haS, hxS⟩
    exact eq_of_mem_of_mem hT hT' hxT hxT' ▸ haT'

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

Goal state before:
pp: α : Type u_1
x y : α
u t✝ : Set α
P : Partition u
ht : t✝ ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : x ∈ t✝
⊢ y ∈ t✝

Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hx]

Goal state after:
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₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ ⊥
⊢ False

Tactic:
simp only [le_bot_iff] at this

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root = ⊥
⊢ False
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✝ : X
⊢ ↑(S.restrict (x✝¹ ⊓ x✝)) = ↑(S.restrict x✝¹) ⊓ ↑(S.restrict x✝)

Tactic:
by simp [S.giRestrict.gc.u_inf]

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)

pp: case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ ∀ (i_1 : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i_1 ×ˢ A)

Tactic:
· intros A hA
    simp only [MeasurableSpace.map_def,
      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]
    exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ ∀ (i_1 : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i_1 ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case neg
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

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

Goal state after:
case neg
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
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 {ω | τ ω < ↑i}

Tactic:
rw [this]; exact @MeasurableSet.empty _ (f i)

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

Goal state before:
pp: case pos.refine_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty

Tactic:
obtain ⟨k, hk_Icc, hk_s⟩ := h

Goal state after:
case pos.refine_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
k : ι
hk_Icc : k ∈ Set.Icc n m
hk_s : u k ω ∈ s
⊢ (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
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 {ω | τ ω < ↑i}

Tactic:
rw [this]; exact @MeasurableSet.empty _ (f i)

Goal state after:
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 : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
simp_rw [hittingBtwn, if_neg h] at hl

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
hl : m < m
⊢ u (hittingBtwn u s n m ω) ω ∈ s
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 ∂μ = ∫ (x : Ω) in s, μ[f (n + 1) | ↑𝒢 n] x ∂μ.trim ⋯

Tactic:
← setIntegral_trim (𝒢.le n) stronglyMeasurable_condExp 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 ∂μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝ : i ∈ ↑(Finset.range N)
⊢ ∀ ⦃y : ℕ⦄,
    y ∈ ↑(Finset.range N) →
      i ≠ y →
        Function.onFun Disjoint (fun k ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          i y

Tactic:
j

Goal state after:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝ : i ∈ ↑(Finset.range N)
j : ℕ
⊢ j ∈ ↑(Finset.range N) →
    i ≠ j →
      Function.onFun Disjoint (fun k ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i
        j
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ MeasurableSet (sᶜ ∩ {ω | τ ω ≤ ↑i})

Tactic:
(_ : sᶜ ∩ {ω | τ ω ≤ i} = (sᶜ ∪ {ω | τ ω ≤ i}ᶜ) ∩ {ω | τ ω ≤ i})

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ MeasurableSet ((sᶜ ∪ {ω | τ ω ≤ ↑i}ᶜ) ∩ {ω | τ ω ≤ ↑i})

Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ sᶜ ∩ {ω | τ ω ≤ ↑i} = (sᶜ ∪ {ω | τ ω ≤ ↑i}ᶜ) ∩ {ω | τ ω ≤ ↑i}