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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
h : Valued.v.restrict (x - y) < Valued.v.restrict (↑p ^ n)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹

Tactic:
Valuation.restrict_lt_iff,

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
h : Valued.v (x - y) < Valued.v (↑p ^ n)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y)) ≤ (↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ (Rat.padicValuation p) (x' - y') < embedding ↑γ

Tactic:
change padicNorm p (x' - y') ≤ _ at h

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : padicNorm p (x' - y') ≤ (↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
⊢ (Rat.padicValuation p) (x' - y') < embedding ↑γ
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
a : ℤ
hq : a ^ 2 = d
ha : q.num = ↑q.den * a
⊢ False

Tactic:
exact hd ⟨a, sq a ▸ hq.symm⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
⊢ ↑m.natAbs ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den

Tactic:
← ZMod.intCast_eq_intCast_iff_dvd_sub

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
⊢ ↑(q₂.num * ↑q₁.den) = ↑(q₁.num * ↑q₂.den)
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
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.y ≤ |a.y|

Tactic:
← abs_of_pos h.2.1,

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : Field K
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra K L
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹² : P.LiesOver p
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : MulSemiringAction Gal(L/K) B
inst✝⁹ : IsGaloisGroup Gal(L/K) A B
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Ring.HasFiniteQuotients A
inst✝³ : P.IsMaximal
D : Type u_5
inst✝² : Field D
inst✝¹ : Algebra D L
inst✝ : IsDecompositionField K L P D
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Finite (A ⧸ p)
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B

Tactic:
rw [← IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L, card_stabilizer_eq p]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.y| < a.x * a₁.y

Tactic:
← abs_of_pos h.2.1,

Goal state after:
case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.y| < a.x * |a₁.y|
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
n k : ℕ
⊢ 2 ^ n ≤ 2 ^ (n + k)

Tactic:
by
      apply pow_right_mono₀
      · simp
      · apply Nat.le_add_right

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ ∏ p ∈ d.primeFactors, s.nu p < ∏ p ∈ d.primeFactors, 1

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

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
⊢ d1 ∈ s.prodPrimes.divisors →
    (∑ x ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
      ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
hd1

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
⊢ (∑ x ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m

Tactic:
have : ∀ f : Fin 4 → ZMod 2, f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i : Fin 4,
      f i ^ 2 + f (swap i 0 1) ^ 2 = 0 ∧ f (swap i 0 2) ^ 2 + f (swap i 0 3) ^ 2 = 0 := by
    decide
  set f : Fin 4 → ℤ := ![a, b, c, d]
  obtain ⟨i, hσ⟩ := this (fun x => ↑(f x)) <| by
    rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
    simp only [Int.cast_add, Int.cast_pow]
    rfl
  set σ := swap i 0
  obtain ⟨x, hx⟩ : (2 : ℤ) ∣ f (σ 0) ^ 2 + f (σ 1) ^ 2 :=
    (CharP.intCast_eq_zero_iff (ZMod 2) 2 _).1 <| by
      simpa only [σ, Int.cast_pow, Int.cast_add, Equiv.swap_apply_right, ZMod.pow_card] using! hσ.1
  obtain ⟨y, hy⟩ : (2 : ℤ) ∣ f (σ 2) ^ 2 + f (σ 3) ^ 2 :=
    (CharP.intCast_eq_zero_iff (ZMod 2) 2 _).1 <| by
      simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using! hσ.2
  refine ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2,
    (f (σ 2) + f (σ 3)) / 2, ?_⟩
  rw [← Int.sq_add_sq_of_two_mul_sq_add_sq hx.symm, add_assoc,
    ← Int.sq_add_sq_of_two_mul_sq_add_sq hy.symm, ← mul_right_inj' two_ne_zero, ← h, mul_add]
  have : (∑ x, f (σ x) ^ 2) = ∑ x, f x ^ 2 := Equiv.sum_comp σ (f · ^ 2)
  simpa only [← hx, ← hy, Fin.sum_univ_four, add_assoc] using! this

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ (toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]
  simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, add_mul]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ ↑(norm y).natAbs

Tactic:
abs_natCast_norm

Goal state after:
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ norm y
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ n = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
rw [h₁, h]; ring

Goal state after:
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 : 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
⊢ ∃ 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:
suffices hx' : x ∈ Ideal.span {a} ⊔ P ^ (i + 1) by
    obtain ⟨y', hy', z, hz, rfl⟩ := Submodule.mem_sup.mp hx'
    obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hy'
    refine ⟨Submodule.Quotient.mk y, ?_⟩
    simp only [Submodule.Quotient.quot_mk_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
      Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff,
      Submodule.coe_sub]
    refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
    rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
      sub_add_cancel_left, map_neg]

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 : 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
⊢ x ∈ span {a} ⊔ P ^ (i + 1)
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x : ℝ
hx : Irrational x
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)

Tactic:
by
  have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
    ((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.isClosedEmbedding_coe_real.isClosedMap).isClosed_range
  have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) := by
    rintro ⟨m, rfl⟩
    simp at hx
  rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩
  refine (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => ?_
  rw [dist_comm] at hlt
  refine hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩
  simp [div_eq_inv_mul]

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

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)

Tactic:
replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ (↑r.den * ↑m + ↑r.num * ↑n) / (↑r.den * ↑n) = ↑m / ↑n + ↑r.num / ↑r.den

Tactic:
add_div,

Goal state after:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑r.den * ↑m / (↑r.den * ↑n) + ↑r.num * ↑n / (↑r.den * ↑n) = ↑m / ↑n + ↑r.num / ↑r.den
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s

Tactic:
by
  simp_rw [← not_bounded_iff, bounded_inter_not H]

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ Disjoint a bᶜ ↔ a ≤ b

Tactic:
← le_compl_iff_disjoint_right,

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ a ≤ bᶜᶜ ↔ a ≤ b
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ ∃ x, Antitone f ∧ Antitone g

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_antitoneOn]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n✝ m✝ : Nucleus X
x✝ y : X
m n : Nucleus X
x : X
⊢ (⇑m ⊓ ⇑n) ((⇑m ⊓ ⇑n) x) ≤ (⇑m ⊓ ⇑n) x

Tactic:
by
      simp only [Pi.inf_apply, map_inf, idempotent]
      exact inf_le_inf inf_le_left inf_le_right

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 β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ f x b

Tactic:
rw [← h']

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 β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_3
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
⊢ ⨅ x ∈ X, f x b = f a b

Tactic:
apply le_antisymm
    · apply iInf₂_le a ha
    · apply le_trans (le_iSup₂ b hb) h

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

Goal state before:
pp: case refine_3.inl
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
ha : ↑a ∉ u
⊢ f ↑a = f₀ a

pp: case refine_3.inr
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
ha : ↑a ∈ u
⊢ f ↑a = f₀ a

Tactic:
· simp [hfdef, ha, h_notMem _ ha]

Goal state after:
case refine_3.inr
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
ha : ↑a ∈ u
⊢ f ↑a = f₀ a
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
n : ℕ
⊢ f 0 + (∑ i ∈ Finset.range n, (f (i + 1) - f i) - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i]) =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])

Tactic:
← Finset.sum_sub_distrib

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ f 0 + ∑ x ∈ Finset.range n, (f (x + 1) - f x - μ[f (x + 1) - f x | ↑ℱ x]) =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])
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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
⊢ martingalePart (f + g) ℱ μ n =ᵐ[μ] f n

Tactic:
refine (eventuallyEq_iff_sub.2 ?_).symm

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✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
⊢ f n - martingalePart (f + g) ℱ μ n =ᵐ[μ] 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : 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 {ω | τ ω ≤ j}

Tactic:
lift j to ι using (ne_top_of_lt hji)
    exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi' : i ≤ m₁
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) ≤ i

Tactic:
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤

Tactic:
simp only [Set.mem_univ, true_and] at h_notMem_s

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), u x ω ∉ s
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) → upcrossings a b f ω < ∞

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
k : ℝ≥0
hk : upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ∞
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case mp
Ω : 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:
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
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
rintro ⟨k, hk⟩

Goal state after:
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.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable fun a ↦ min (τ a) ↑i

pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable fun a ↦ min (min (τ a) (π a)) ↑i

Tactic:
· exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable fun a ↦ min (min (τ a) (π a)) ↑i