mathlib-initiative/mathlib-tactics huggingface dataset:
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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
⊢ ∀ (p : Nat.Primes), u p +ᵥ E =ᵐ[μ] E

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (cardinalGenerate g hc) c

Tactic:
by

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
⊢ ⋂₀ ∅ ⊆ Set.univ

Tactic:
by

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

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 : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), #↑(T s a) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
⊢ Set.univ ∈ {s | r.core s ∈ l}

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ x✝ ∩ y✝ ∈ {s | r.core s ∈ l}

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter α
⊢ (rmap s (rmap r l)).sets = (rmap (r.comp s) l).sets

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
by

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 ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (r.comp s) l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
i : Fin n
⊢ insertNth 0 x f i.succ.castSucc ≤ insertNth 0 x f i.succ.succ

Tactic:
simpa using hf i.castSucc_le_succ

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
⊢ Monotone (insertNth 0 x f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
x : α
hx : x < f 0
⊢ StrictMono (insertNth 0 x f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : j < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ

Tactic:
obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hj)

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin n
hj : j.castSucc < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc.castSucc ≤ i.castSucc.succ.insertNth x f j.castSucc.succ
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r ≤ s.encard

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : ↑n ≤ s.chainHeight r
h' : n = 0
⊢ ∅ ⊆ s ∧ ∅.encard = ↑n ∧ IsChain r ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : ↑n ≤ s.chainHeight r
h' : ¬n = 0
⊢ ∃ t ⊆ s, IsChain r t ∧ ↑n ≤ t.encard

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : ↑n ≤ s.chainHeight r
⊢ ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ Monotone (i.castSucc.succ.insertNth x f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∅ ⊆ s ∧ IsChain r ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty { t // t ⊆ s ∧ IsChain r t }
⊢ ⨆ i, ?m.28 i < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
⊢ ¬IsChain r t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : j < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

Tactic:
obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hj)

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin n
hj : j.castSucc < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc.castSucc < i.castSucc.succ.insertNth x f j.castSucc.succ
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: case hUnion
α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ {s | #↑s < c}) → ⋃₀ S ∈ {s | #↑s < c}

pp: case hmono
α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ ∀ t ∈ {s | #↑s < c}, ∀ s ⊆ t, s ∈ {s | #↑s < c}

Tactic:
· refine fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_
    apply iSup_lt_of_lt_cof_ord _ fun i ↦ hSc i.1 i.2
    rwa [hreg.cof_ord]

Goal state after:
case hmono
α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ ∀ t ∈ {s | #↑s < c}, ∀ s ⊆ t, s ∈ {s | #↑s < c}
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ Filter α

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ cocardinal α isRegular_aleph0 = cofinite

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = 0 ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ s.chainHeight r ≤ t.chainHeight r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain (flip r) a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ r x y ∨ r y x) x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ StrictMono (i.castSucc.succ.insertNth x f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ flip r x y ∨ flip r y x) x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight (flip r) = s.chainHeight r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ (⇑e '' s).chainHeight r'
a : Set β
ha₁ : a ⊆ ⇑e '' s
ha₂ : a.encard = ↑n
ha₃ : IsChain r' a
⊢ a ⊆ range ⇑e

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #↑S < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ ⋂₀ S ∈ cocardinal α hreg

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
⊢ ⇑e '' a ⊆ ⇑e '' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
⊢ (⇑e '' s).chainHeight r' = s.chainHeight r

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, #↑i < c ∧ iᶜ ⊆ s
_t : Set α
htf : #↑_t < c
hts : _tᶜ ⊆ s
⊢ #↑sᶜ < c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
⊢ (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) = fun x y ↦ r ↑x ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 ≤ x2) = s.chainHeight fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
⊢ Monotone ((last (n + 1)).insertNth x f)

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, #↑i < c ∧ iᶜ ⊆ s
_t : Set α
htf : #↑_t < c
hts : _tᶜ ⊆ s
⊢ s ∈ cocardinal α hreg

Tactic:
by

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LT α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 < x2) = s.chainHeight fun x1 x2 ↦ x1 < x2

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
p : α → Prop
⊢ (∃ᶠ (x : α) in cocardinal α hreg, p x) ↔ c ≤ #↑{x | p x}

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ∈ cocountable ↔ sᶜ.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
⊢ IsRegular ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜ = ⊤

Tactic:
compl_bot

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
⊢ ⊤ = ⊤
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
⊢ IsRegular ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⊓ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⇨ b)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ ⊥ᶜ = ⊤

Tactic:
compl_bot

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ ⊤ = ⊤
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ a ⊔ aᶜ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
x : α
hx : f (last n) < x
⊢ StrictMono ((last (n + 1)).insertNth x f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : Regular α
⊢ ↑((a ⊔ b) ⊓ (a ⊔ c)) ≤ ↑(a ⊔ b ⊓ c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a b : α
n : ℤ
⊢ ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a b : α
n : ℤ
⊢ ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉ ⌈b⌉

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
a : Regular α
⊢ ⊤ ≤ ⊥ᶜ

Tactic:
compl_bot

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
a : Regular α
⊢ ⊤ ≤ ⊤
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a b : α
n : ℤ
⊢ ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉ ⌊b⌋

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
a : Regular α
⊢ ↑⊤ ≤ ↑(a ⊔ aᶜ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a b : α
n : ℤ
⊢ ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋ ⌈b⌉

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℤ
⊢ ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℤ
⊢ ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
b : α
n : ℤ
⊢ ↑n ∈ Set.Iic b ↔ n ∈ Set.Iic ⌊b⌋

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b : Regular α
⊢ ↑(a ⇨ b) = ↑(b ⊔ aᶜ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
b : α
n : ℤ
⊢ ↑n ∈ Set.Iio b ↔ n ∈ Set.Iio ⌈b⌉

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : FloorSemiring α
a b : α
n : ℕ
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
⊢ ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
hb : 0 ≤ b
⊢ ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
b : α
n : ℕ
hb : 0 ≤ b
⊢ ↑n ∈ Set.Iic b ↔ n ∈ Finset.Iic ⌊b⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
b : α
n : ℕ
⊢ ↑n ∈ Set.Iio b ↔ n ∈ Finset.Iio ⌈b⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
⊢ (∀ᵐ (x : 𝕊), x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊), x ∈ addWellApproximable 𝕊 δ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Icc a b).ncard = b + 1 - a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ico a b).ncard = b - a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioc a b).ncard = b - a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioo a b).ncard = b - a - 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (uIcc a b).ncard = (↑b - ↑a).natAbs + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: b : ℕ
⊢ (Iic b).ncard = b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: b : ℕ
⊢ (Iio b).ncard = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 1).1 ≤ (1, 1).2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 2).1 ≤ (1, 2).2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 3).1 ≤ (1, 3).2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (2, 2).1 ≤ (2, 2).2

Tactic:
by

Goal state after: