mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_1
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
⊢ x * ↑r ≠ ↑(r.num * m) / ↑(r.den • id n)

Tactic:
rw [A]; simp [hne, hr]

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:
;

Goal state after:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (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))

Tactic:
;

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (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))
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ≠ 0

Tactic:
;

Goal state after:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ≠ 0
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (↑a).val = val 0
⊢ False

Tactic:
;

Goal state after:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (↑a).val = val 0
⊢ False
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ a₁✝ = a₂✝

Tactic:
;

Goal state after:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ a₁✝ = a₂✝
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ ↑a₁✝ = ↑a₂✝

Tactic:
;

Goal state after:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ ↑a₁✝ = ↑a₂✝
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
⊢ False

Tactic:
;

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 = 0
⊢ False
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:
;

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 = 0
⊢ b = 0
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
⊢ ↑a = ↑(↑a).val

Tactic:
;

Goal state after:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
⊢ ↑a = ↑(↑a).val
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
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) ∧
    |x + ↑r - ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p

Tactic:
;

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
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) ∧
    |x + ↑r - ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Unbounded (fun x1 x2 ↦ x1 < x2) (s ∩ {b | a < b}) ↔ Unbounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_lt_inter_lt a

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

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

Tactic:
;

Goal state after:
⊢ ∀ (i : ℤ),
    volume
        ((fun x ↦ x + ↑i) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

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

Tactic:
;

Goal state after:
m : ℤ
⊢ volume
      ((fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: m : ℤ
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
;

Goal state after:
m : ℤ
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    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
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n

Tactic:
;

Goal state after:
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
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n
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
⊢ -↑m / ↑n - -x = x - ↑m / ↑n

Tactic:
;

Goal state after:
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
⊢ -↑m / ↑n - -x = x - ↑m / ↑n
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p : ℝ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False

Tactic:
;

Goal state after:
p : ℝ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0

Tactic:
;

Goal state after:
case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
Module: Mathlib.Order.Category.CompleteLat

Goal state before:
pp: α β : CompleteLat
e : ↑α ≃o ↑β
a✝ : ↑α
⊢ (ConcreteCategory.hom
        (ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
          ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : CompleteLat
e : ↑α ≃o ↑β
a✝ : ↑α
⊢ (ConcreteCategory.hom
        (ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
          ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.CompleteLat

Goal state before:
pp: α β : CompleteLat
e : ↑α ≃o ↑β
a✝ : ↑β
⊢ (ConcreteCategory.hom
        (ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
          ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : CompleteLat
e : ↑α ≃o ↑β
a✝ : ↑β
⊢ (ConcreteCategory.hom
        (ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
          ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
⊢ False

Tactic:
;

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False

Tactic:
;

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ b ^ m ∈ {u | orderOf u = orderOf b}

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ b ^ m ∈ {u | orderOf u = orderOf b}
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
⊢ (ConcreteCategory.hom m) t =
    (ConcreteCategory.hom
        { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ })
      t

Tactic:
;

Goal state after:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
⊢ (ConcreteCategory.hom m) t =
    (ConcreteCategory.hom
        { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ })
      t
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x✝ : s.pt.carrier
⊢ (ConcreteCategory.hom
        ({ toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ } ≫ (equalizer f g).ι))
      x✝ =
    (ConcreteCategory.hom s.ι) x✝
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:
;

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.NumberTheory.WellApproximable

Goal state before:
pp: case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
;

Goal state after:
case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : gcd m n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
;

Goal state after:
case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : gcd m n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑α.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑α.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑β.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑β.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 β)) a✝
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left✝ : gcd m n = 1
right✝ : ‖x - ↑(↑m / ↑n)‖ < δ n
⊢ 0 < n

Tactic:
;

Goal state after:
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left✝ : gcd m n = 1
right✝ : ‖x - ↑(↑m / ↑n)‖ < δ n
⊢ 0 < n
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
p : ℕ
hp : Nat.Prime p
⊢ addOrderOf (u ⟨p, hp⟩) = ↑⟨p, hp⟩

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
p : ℕ
hp : Nat.Prime p
⊢ addOrderOf (u ⟨p, hp⟩) = ↑⟨p, hp⟩
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑α.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑α.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑β.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑β.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } =
    (fun L ↦ L.carrier) M
⊢ { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } = M

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } =
    (fun L ↦ L.carrier) M
⊢ { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } = M
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice✝¹ : Sublattice α
sSupClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sSup s ∈ toSublattice✝¹.carrier
sInfClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sInf s ∈ toSublattice✝¹.carrier
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
⊢ { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice✝¹ : Sublattice α
sSupClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sSup s ∈ toSublattice✝¹.carrier
sInfClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sInf s ∈ toSublattice✝¹.carrier
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
⊢ { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }