mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
this : ↑p ∣ { re := ↑k, im := 1 } ∨ ↑p ∣ { re := ↑k, im := -1 }
⊢ False

Tactic:
tauto

Goal state after:
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
powQuotSuccInclusion_apply_coe,

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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case 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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz✝⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

Tactic:
powQuotSuccInclusion_apply_coe,

Goal state after:
case 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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : ↑⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz✝⟩ = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case 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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : z - (a * x - a * y) ∈ P ^ e
⊢ x - y ∈ P

Tactic:
← mul_sub

Goal state after:
case 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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ↑((p.powQuotSuccInclusion P i) ⟨(Quotient.mk (P ^ e)) (-z), ⋯⟩) =
    (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

Tactic:
powQuotSuccInclusion_apply_coe,

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
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ↑⟨(Quotient.mk (P ^ e)) (-z), ⋯⟩ = (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖deriv (fun x ↦ eval x fR) y‖ ≤ |eval xm (derivative fR)|

Tactic:
rw [fR.deriv]; exact hM h

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

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|

Tactic:
show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ f.natDegree * |eval (↑z / ↑↑(a + 1)) fR|
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case mul
m n : ℕ
hm : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * n

Tactic:
rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩

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

Goal state before:
pp: x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 1 < x * ↑n + 2

Tactic:
linarith

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

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ C / ↑n ^ p * |↑r| = ↑r.den ^ p * (↑|r| * C) / (↑r.den ^ p * ↑n ^ p)

pp: case refine_2.hx
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑r.den

pp: case refine_2.hy
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑n

Tactic:
mul_div_mul_left,

Goal state after:
case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ C / ↑n ^ p * |↑r| = ↑|r| * C / ↑n ^ p

case refine_2.hc
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ↑r.den ^ p ≠ 0

case refine_2.hx
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑r.den

case refine_2.hy
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑n
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ b = 0

Tactic:
apply_fun val at h

Goal state after:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : (↑b).val = val 0
⊢ b = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -x ≠ ↑(-m) / ↑n

Tactic:
by simp [neg_div, hne]

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

Goal state before:
pp: r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ 1 - r ≠ 0

Tactic:
linarith

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

Goal state before:
pp: case refine_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ 1 - r < -1

Tactic:
linarith

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

Goal state before:
pp: case refine_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ -r < -1

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
simp only [mem_approx_add_orderOf_iff, mem_ofPred_eq, ball, dist_eq_norm,
    AddCircle.addOrderOf_eq_pos_iff hn, mul_one]
  constructor
  · rintro ⟨y, ⟨m, hm₁, hm₂, rfl⟩, hx⟩; exact ⟨m, hm₁, hm₂, hx⟩
  · rintro ⟨m, hm₁, hm₂, hx⟩; exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ≤ b ∧ ¬b ≤ a ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case e_p
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := ⋯
μ : Measure 𝕊 := ⋯
u : Nat.Primes → 𝕊 := ⋯
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := ⋯
X : ℕ → Set 𝕊 := ⋯
A : ℕ → Set 𝕊 := ⋯
B : ℕ → Set 𝕊 := ⋯
C : ℕ → Set 𝕊 := ⋯
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
p n : ℕ
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ s

Tactic:
rw [← h.eq]
  exact lowerPolar_upperPolar_monotone r hs'

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_2.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ ∃ r ∈ c, r x z

Tactic:
exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
this : countableSupClosure s = {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ a ∈ countableSupClosure s ↔ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a

Tactic:
simp [this]

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s✝ t✝ : Set α
a✝¹ : CardinalGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s✝
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #↑a < c ∧ ⋂₀ a ⊆ s✝ → a ⊆ g ∧ #↑a < c ∧ ⋂₀ a ⊆ t✝

Tactic:
tauto

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ IsGreatest {f | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)

Tactic:
refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩
  rintro f ⟨fct, hf⟩
  rwa [le_cardinalGenerate_iff_of_cardinalInterFilter]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
contra : ¬0 ≤ δ / 2
this : μ (closedBall 0 (δ / 2)) = 0
⊢ (n + 1) • μ (closedBall 0 (δ / 2)) ≤ 0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ MonovaryOrder f g i j → MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
rw [MonovaryOrder]; exact _root_.trans

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
⊢ ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
intro a₁ a₂

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
⊢ a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂)

Tactic:
gcongr; exacts [le_sup_left, le_sup_right]

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
hab : f a = f b
⊢ P.Rel b (f b)

Tactic:
refine hf.rel_apply <| by_contra fun hb ↦ ?_

Goal state after:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
hab : f a = f b
hb : b ∉ u
⊢ False
Module: Mathlib.Order.SuccPred.Tree

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

Tactic:
simp [this]

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
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ (fun i a ↦ ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c

Tactic:
ext (i a)

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁴ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
i : ι
a : Ω
⊢ ∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a
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
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ IsStronglyProgressive f fun i a ↦ ∏ c ∈ s, U c i a

Tactic:
convert! IsStronglyProgressive.finsetProd' h using 1; ext (i a); simp only [Finset.prod_apply]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
rw [← Set.Ioi_sdiff_Ioi, (by simp : (Set.Ioi i \ Set.Ioi j) ×ˢ s
      = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s), ← Set.prod_sdiff_prod]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)
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
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : ↑(Set.singleton (n + 1)) × Ω
⊢ i < ↑p.1 → p.2 ∉ A

Tactic:
rw [p.1.2]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : ↑(Set.singleton (n + 1)) × Ω
⊢ i < n + 1 → p.2 ∉ A
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : ↑(Set.singleton (n + 1)) × Ω
hp2 : p.2 ∈ A
⊢ i < ↑p.1 ↔ p.1 = ⟨n + 1, ⋯⟩

Tactic:
rw [p.1.2]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : ↑(Set.singleton (n + 1)) × Ω
hp2 : p.2 ∈ A
⊢ i < n + 1 ↔ p.1 = ⟨n + 1, ⋯⟩
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
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑ℱ i] ω ≥ 0
n : ℕ
⊢ predictablePart f ℱ μ n ω + μ[f (n + 1) - f n | ↑ℱ n] ω ≥ predictablePart f ℱ μ n ω

Tactic:
h n,

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
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | ↑ℱ i] ω ≥ 0
n : ℕ
⊢ predictablePart f ℱ μ n ω + 0 ≥ predictablePart f ℱ μ n ω
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
⊢ Submartingale f ℱ μ

Tactic:
by
  refine ⟨hadp, fun i j hij => ?_, hint⟩
  suffices f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] by exact ae_le_of_ae_le_trim this
  suffices 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] - f i by
    filter_upwards [this] with x hx
    rwa [← sub_nonneg]
  refine ae_nonneg_of_forall_setIntegral_nonneg
    ((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i))
      fun s hs _ => ?_
  specialize hf i j hij s hs
  rwa [← setIntegral_trim _ (stronglyMeasurable_condExp.sub <| hadp i) hs,
    integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
    setIntegral_condExp (ℱ.le i) (hint j) hs]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω

Tactic:
simp only [lowerCrossingTime, le_hittingBtwn upperCrossingTime_le ω]

Goal state after: