mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))

Tactic:
by

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)

Tactic:
by

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

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x

Tactic:
by

Goal state after:
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)
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: ⊢ volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x✝ : ℝ
h₁ : ∀ p > 2, ¬LiouvilleWith p x✝
h₂ : Liouville x✝
⊢ 3 > 2

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x

Tactic:
by

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

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

Tactic:
by

Goal state after:
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|
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m ↦ 1 / ↑b ^ m) atTop (𝓝 0)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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|
⊢ ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedGroup A
n : ℕ
δ : ℝ
a : A
⊢ a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ ball b δ

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : Liouville x
n : ℕ
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
by

Goal state after:
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 * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ b ^ m ∈ {y | orderOf y = n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
by

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

Goal state before:
pp: X : Frm
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

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

Goal state before:
pp: X Y Z : Frm
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

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

Goal state before:
pp: X Y : Frm
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

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

Goal state before:
pp: X Y : Frm
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

Tactic:
by

Goal state after:
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
⊢ m = { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ }

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ i ∈ c, f i = g i
⊢ f (ωSup c) = g (ωSup c)

Tactic:
by

Goal state after:
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 f) ((ConcreteCategory.hom s.ι) x) = (ConcreteCategory.hom g) ((ConcreteCategory.hom s.ι) x)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ∀ {b : A}, orderOf b = n → orderOf (a * b) = n

Tactic:
by

Goal state after:
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, ⋯⟩
⊢ Surjective f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ

Tactic:
by

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

Goal state before:
pp: X : FinBddDistLat
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

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

Goal state before:
pp: X Y Z : FinBddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

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

Goal state before:
pp: X Y : FinBddDistLat
e : X ≅ Y
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

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

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

Goal state before:
pp: X Y : FinBddDistLat
e : X ≅ Y
s : ↑Y.toDistLat
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

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

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
⊢ 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' := ⋯ }) =
    𝟙 α

Tactic:
by

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

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
⊢ 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' := ⋯ }) =
    𝟙 β

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IncompRel rᶜ = AntisymmRel r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ IncompRel rᶜ a b ↔ AntisymmRel r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬SymmGen r a b ↔ IncompRel r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬IncompRel r a b ↔ SymmGen r a b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Total r
a b : α
⊢ ¬IncompRel r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
h : IncompRel r a b
⊢ a ≠ b

Tactic:
rintro rfl
  exact h.1 <| refl_of r a

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
h : IncompRel r a b
⊢ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: δ : ℕ → ℝ
x : UnitAddCircle
⊢ x ∈ addWellApproximable UnitAddCircle δ ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Order.Comparable

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : Nat.Primes), addOrderOf (u p) = ↑p

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : FinBoolAlg
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (forget₂ FinBoolAlg FinPartOrd).map a₁✝ = (forget₂ FinBoolAlg FinPartOrd).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

Goal state after:
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)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
⊢ Tendsto (addOrderOf ∘ u) atTop atTop

Tactic:
by

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

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
⊢ 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' := ⋯ })) =
    𝟙 α

Tactic:
by

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

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
⊢ 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' := ⋯ })) =
    𝟙 β

Tactic:
by

Goal state after:
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)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
⊢ NullMeasurableSet E μ

Tactic:
by

Goal state after:
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)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
⊢ ∀ (p : ℕ), E = A p ∪ B p ∪ C p

Tactic:
by

Goal state after:
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)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
⊢ ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨅ i, f i ↔ ∀ (i : I), x ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨆ i, f i ↔ ∃ i, x ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∉ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊔ y = sSup {x, y}
z : α
hz : z ∈ {x, y}
⊢ z ∈ carrier

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
⊢ sInf s i = ⨅ e, ↑e i

Tactic:
by

Goal state after:
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)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y ↦ p • y
this : f '' A p ⊆ blimsup (fun n ↦ approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n ↦ 0 < n ∧ ¬p ∣ n
⊢ A ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ A ↑⟨p, hp⟩ =ᵐ[μ] univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊔ y = sSup {x, y}
⊢ x ⊔ y ∈ carrier

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ sInf s i ≤ e i

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ sInf s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y ∈ carrier

Tactic:
by

Goal state after: