mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : b * y ≤ c
⊢ b * y ≤ c

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : b * y ≤ c
⊢ b * y ≤ c
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ∈ f

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ∈ f
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * y ≤ b
⊢ a * y ≤ b

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * y ≤ b
⊢ a * y ≤ b
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
f : Filter α
⊢ f = f

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f ≤ g⁻¹ ↔ f ≤ g⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : c * y ≤ d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : c * y ≤ d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓
      comap (Prod.map (fun x ↦ Prod.snd ∘ x) fun x ↦ Prod.snd ∘ x) (𝓤 (α → γ))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓
      comap (Prod.map (fun x ↦ Prod.snd ∘ x) fun x ↦ Prod.snd ∘ x) (𝓤 (α → γ))
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ 1

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ 1
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : s = univ
⊢ s = univ

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : s = univ
⊢ s = univ
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ i, UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)) =
    ⨅ i, uniformSpace α ((i : ι) → δ i) 𝔖

Tactic:
]

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ i, UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)) =
    ⨅ i, uniformSpace α ((i : ι) → δ i) 𝔖
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ {a} ∈ f

Tactic:
]

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ {a} ∈ f
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) (uniformSpace α (δ i) 𝔖) =
    UniformSpace.comap (fun x ↦ Function.eval i ∘ x) (uniformSpace α (δ i) 𝔖)

Tactic:
]

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) (uniformSpace α (δ i) 𝔖) =
    UniformSpace.comap (fun x ↦ Function.eval i ∘ x) (uniformSpace α (δ i) 𝔖)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ {b} ∈ g

Tactic:
]

Goal state after:
case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ {b} ∈ g
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure b = pure b

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}
huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}
huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1

Tactic:
]

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ Ioi 0 = Ioi 0

Tactic:
]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ Ioi a = Ioi a

Tactic:
]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ 0 ∈ s

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ 0 ∈ s
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Icc (a * c + b) (a * d + b) = Icc (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
]

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace X
inst✝¹ : SMul M X
inst✝ : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact ((fun x ↦ x.1 • x.2) '' k ×ˢ u)

Tactic:
]

Goal state after:
M : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace X
inst✝¹ : SMul M X
inst✝ : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact ((fun x ↦ x.1 • x.2) '' k ×ˢ u)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Ico (a * c + b) (a * d + b) = Ico (a * c + b) (a * d + b)

Tactic:
]

Goal state after: