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

Goal state before:
pp: 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
this✝¹ : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this✝ :
  (f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d) ^ 2 + (f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c) ^ 2 +
        (f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b) ^ 2 +
      (f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a) ^ 2 =
    ↑(m * r) * ↑(m * p)
this : ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2 = 0
⊢ ↑m ∣ f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c

Tactic:
simpa using

Goal state after:
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
this✝¹ : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this✝ :
  (f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d) ^ 2 + (f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c) ^ 2 +
        (f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b) ^ 2 +
      (f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a) ^ 2 =
    ↑(m * r) * ↑(m * p)
this : ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2 = 0
⊢ ↑a * ↑a + (↑b * ↑b + (↑c * ↑c + ↑d * ↑d)) = 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_1
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
⊢ p + p * f.natDegree - p - 1 ≤ p * f.natDegree - 1

Tactic:
add_tsub_cancel_left

Goal state after:
case h.right.refine_1
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
⊢ p * f.natDegree - 1 ≤ p * f.natDegree - 1
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Tactic:
simpa using

Goal state after:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ remainder (↑m) n < ((↑m ^ n !) ^ n)⁻¹
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x ↑r

Tactic:
simpa using

Goal state after:
x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x (↑r.num / ↑r.den)
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 : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p

Tactic:
refine ⟨hle, m, hne, hlt.trans_le ?_⟩

Goal state after:
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ max C 1 / ↑n ^ p
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
⊢ ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)

Tactic:
simpa using

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
⊢ ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset

Tactic:
simpa using

Goal state after:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ c' r ∈ Multiset.map c' (f.aroots ℂ)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h✝ : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset
h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0

Tactic:
simpa using

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h✝ : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset
h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty
⊢ c' r ≤ (Multiset.map c' (f.aroots ℂ)).toFinset.max' ⋯
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x

Tactic:
simpa using

Goal state after:
p x : ℝ
r : ℚ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < (↑b ^ (2 + 1 / (↑n + 1)))⁻¹
⊢ ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))

Tactic:
← one_div,

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / (↑n + 1))
⊢ ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 2 ≤ 2 + 1 / ↑(n + 1)

Tactic:
simpa using

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 0 ≤ ↑n + 1
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).val = val 0
⊢ b = 0

Tactic:
simpa using

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.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = -1

Tactic:
refine
    calc
      ((p - 1)! : ZMod p) = ∏ x ∈ Ico 1 (succ (p - 1)), (x : ZMod p) := by
        rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
      _ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := ?_
      _ = -1 := by
        simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
  have hp : 0 < p := (Fact.out (p := p.Prime)).pos
  symm
  refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
  · intro a ha
    rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]
    constructor
    · apply Nat.pos_of_ne_zero; rw [← @val_zero p]
      intro h; apply Units.ne_zero a (val_injective p h)
    · exact val_lt _
  · intro _ _ _ _ h; rw [Units.ext_iff]; exact val_injective p h
  · intro b hb
    rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
    refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
    · intro h; apply hb.1; apply_fun val at h
      simpa only [val_cast_of_lt hb.right, val_zero] using h
    · simp only [val_cast_of_lt hb.right, Units.val_mk0]
  · rintro a -; simp only [cast_id, natCast_val]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ ∀ (a a_1 : Set α), (∀ x ∈ a_1, ∀ x_1 ∈ a, x_1 ≤ x) ↔ ∀ x ∈ a, ∀ x_1 ∈ a_1, x ≤ x_1
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
h : LiouvilleWith p (x + ↑r)
⊢ LiouvilleWith p x

Tactic:
simpa using

Goal state after:
p x : ℝ
r : ℚ
h : LiouvilleWith p (x + ↑r)
⊢ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ (↑n)⁻¹ ≤ |↑M - ↑m / ↑n|

Tactic:
← one_div,

Goal state after:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 / ↑n ≤ |↑M - ↑m / ↑n|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

Tactic:
simpa using

Goal state after:
⊢ volume (⋃ i, ⋃ (_ : i > 2), {x | LiouvilleWith i x}) = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ volume {x | Liouville x} = 0

Tactic:
simpa using

Goal state after:
⊢ volume {x | Liouville x} = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑↑b| < 1 / ↑↑b ^ n

Tactic:
simpa using

Goal state after:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑b| < (↑b ^ n)⁻¹
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
hf : Surjective f
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
hf : Surjective f
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a < b ∨ a = b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a < b ∨ a = b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b
Module: Mathlib.Order.CompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

Tactic:
refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩
  rw [hda.unique hd.isLUB_sSup]
  exact h hne hd

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ↑(sSup (range f)) = ⨆ i, ↑(f i)

Tactic:
coe_sSup',

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ⨆ N ∈ range f, ↑N = ⨆ i, ↑(f i)
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sSup s ∈ ⇑f ⁻¹' ↑L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sSup (⇑f '' s) ∈ L
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sInf s ∈ ⇑f ⁻¹' ↑L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sInf (⇑f '' s) ∈ L
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
y : α
hy : y ∈ c'.extent
⊢ r' y x

Tactic:
apply Not.imp_symm <| Std.Trichotomous.trichotomous x y (hx <| mem_extent_of_rel_extent · hy)

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
y : α
hy : y ∈ c'.extent
⊢ ¬x = y
Module: Mathlib.Order.Completion

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ principal a ≤ principal b ↔ a ≤ b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ (factorEmbedding f) (principal x) = f x

Tactic:
rw [factorEmbedding_apply]
  apply le_antisymm (by simp)
  rw [le_sSup_iff]
  refine fun y hy ↦ hy ?_
  simp

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent ⊆ t
⊢ c.intent ⊆ (ofAttributes r t).intent

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent ⊆ t
⊢ c.intent ⊆ upperPolar r (lowerPolar r t)
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c ∉ a.left, c ∈ b.left
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c ∈ a.right, c ∉ b.right
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hac, hcb⟩ := lt_iff_exists.mp h
    obtain ⟨d, had, hdc⟩ := lt_iff_exists'.mp hac
    simp only [principal_lt_principal] at hdc
    obtain ⟨u, _, _⟩ := DenselyOrdered.dense d c hdc
    exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
obtain rfl | ho := ho.eq_or_lt
  · exact ⟨a, ha, rfl⟩
  · revert ho
    refine ha.recOn fun a ha IH ho ↦ ?_
    rw [rank_eq, Ordinal.lt_iSup_iff] at ho
    obtain ⟨⟨b, hb⟩, ho⟩ := ho
    rw [Order.lt_succ_iff] at ho
    obtain rfl | ho := ho.eq_or_lt
    exacts [⟨b, ha b hb, rfl⟩, IH _ hb ho]

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

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter β
inst✝ : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #↑S < c
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ f ⁻¹' ⋂ i ∈ S, t i ⊆ ⋂₀ S

Tactic:
simpa using

Goal state after:
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝¹ : CardinalInterFilter l✝ c
l : Filter β
inst✝ : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #↑S < c
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ∀ t' ∈ S, ⋂ i ∈ S, f ⁻¹' t i ⊆ t'
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ #↑{s} < c ∧ ⋂₀ {s} ⊆ s

Tactic:
simpa using

Goal state after:
case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ 1 < c
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.superset
α : 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✝
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ t✝

Tactic:
exact Exists.imp (by tauto) ih

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

Goal state before:
pp: case mp
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂

Tactic:
simpa using

Goal state after:
case mp
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) → ∀ (x : Set α), ∀ x_1 ∈ l₂, r.core x_1 ⊆ x → x ∈ l₁
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁

Tactic:
simpa using

Goal state after:
case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α), ∀ x_1 ∈ l₂, r.core x_1 ⊆ x → x ∈ l₁) → ∀ s ∈ l₂, r.core s ∈ l₁
Module: Mathlib.Order.Filter.Partial

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

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

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

Goal state before:
pp: case mp
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } →
    ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
simpa using

Goal state after:
case mp
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α), ∀ x_1 ∈ l₂, r.preimage x_1 ⊆ x → x ∈ l₁) → ∀ s ∈ l₂, r.preimage s ∈ l₁
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.preimage s ∈ l₁) →
    l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ }

Tactic:
simpa using

Goal state after:
case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.preimage s ∈ l₁) → ∀ (x : Set α), ∀ x_1 ∈ l₂, r.preimage x_1 ⊆ x → x ∈ l₁