mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (b - p) = toIocDiv hp a b - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (a - p) b = toIocDiv hp a b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp a (b - c) = toIocDiv hp (a + c) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
⊢ univᶜ ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s t : Set X
hs : sᶜ ∈ T
ht : tᶜ ∈ T
⊢ (s ∩ t)ᶜ ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ (⋃₀ s)ᶜ ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
⊢ t = t'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (s₁ ∪ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
⊢ IsOpen[inst✝] s ↔ ∀ (i : α), IsOpen[inst✝] (f i ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Set α → Filter β
⊢ ⊤.lift g = g univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
⊢ (f.lift g).HasBasis (fun i ↦ p i.fst ∧ pg i.fst i.snd) fun i ↦ sg i.fst i.snd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i ∈ f, ∃ x ∈ g i, id x ⊆ s) ↔ ∃ t ∈ f, s ∈ g t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
h : ∀ t ∈ s, IsOpen[inst✝] t
⊢ IsOpen[inst✝] (⋂₀ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
⊢ ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ comap m (f.lift g) = f.lift (comap m ∘ g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hm : Monotone g
⊢ (f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g h : Set α → Filter β
⊢ (f.lift fun x ↦ g x ⊓ h x) = f.lift g ⊓ f.lift h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : Prop
⊢ IsOpen[inst✝] {_x | p}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u_2
t₁ t₂ : TopologicalSpace X
⊢ t₁ = t₂ ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] s₁ → IsClosed[inst✝] s₂ → IsClosed[inst✝] (s₁ ∪ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
⊢ (∀ t ∈ s, IsClosed[inst✝] t) → IsClosed[inst✝] (⋂₀ s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + m • p) b = toIocMod hp a b + m • p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] sᶜ ↔ IsOpen[inst✝] s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed[inst✝] s₁
h₂ : IsClosed[inst✝] s₂
⊢ IsClosed[inst✝] (s₁ ∩ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed[inst✝] (f i)
⊢ IsClosed[inst✝] (⋃ i ∈ s, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
ι : Sort v
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ IsClosed[inst✝¹] (⋃ i, s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
hf : f.HasBasis p s
hh : Monotone h
t : Set β
⊢ (∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : β → γ
hh : Monotone h
⊢ f.lift (map m ∘ 𝓟 ∘ h) = f.lift' (image m ∘ h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p q : X → Prop
hp : IsOpen[inst✝] {x | p x}
hq : IsClosed[inst✝] {x | q x}
⊢ IsClosed[inst✝] {x | p x → q x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
⊢ comap m (f.lift' h) = f.lift' (preimage m ∘ h)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (pure a).lift' h = 𝓟 (h {a})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ ⊥.lift' h = 𝓟 (h ∅)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ (f.lift fun s ↦ (𝓟 (g s)).lift h) = f.lift fun s ↦ h (g s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
s : Set β
⊢ f.lift' h ⊓ 𝓟 s = f.lift' fun t ↦ h t ∩ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
⊢ (∀ s ∈ f, (𝓟 (h s)).NeBot) ↔ ∀ s ∈ f, (h s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Set β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b + p) = toIcoMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a + p) b = toIcoMod hp a b + p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, Tendsto g f (𝓝 x)
⊢ f.limUnder g = Classical.choice hX

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b + p) = toIocMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a + p) b = toIocMod hp a b + p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (p + b) = toIocMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b - p) = toIcoMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a - p) b = toIcoMod hp a b - p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b - p) = toIocMod hp a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a - p) b = toIocMod hp a b - p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (-b) = p - toIocMod hp (-a) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (-a) b = p - toIocMod hp a (-b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (-b) = p - toIcoMod hp (-a) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (-a) b = p - toIcoMod hp a (-b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = f.lift fun s ↦ g.lift' fun t ↦ s ×ˢ t

Tactic:
by

Goal state after: