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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 (a, b) = (𝓤 α).lift' fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}

Tactic:
by
  rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
  · exact fun s => monotone_const.set_prod monotone_preimage
  · refine fun t => Monotone.set_prod ?_ monotone_const
    exact monotone_preimage (f := fun y => (y, a))

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1) ∧ Tendsto Prod.snd f✝ (𝓝 x2)

Tactic:
constructor

Goal state after:
case left
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1)

case right
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.snd f✝ (𝓝 x2)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ (fun x ↦ (f x.1, f x.2)) =ᶠ[𝓟 (s ×ˢ s)] fun x ↦ (g x.1, g x.2)

Tactic:
filter_upwards [mem_principal_self _] with ⟨a, b⟩ ⟨ha, hb⟩ using by simp [h ha, h hb]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
⊢ Inseparable a b

Tactic:
inseparable_iff_clusterPt_uniformity

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
⊢ (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t

Tactic:
ext

Goal state after:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (entourageProd u v).image (s ×ˢ t) ↔ x✝ ∈ u.image s ×ˢ v.image t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
constructor

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α

Tactic:
by simp [eq_comm, Filter.ext_iff, subset_def, h]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x : α ⊕ β
⊢ 𝓝 x = comap (Prod.mk x) (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β))

Tactic:
ext

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
x : α ⊕ β
s✝ : Set (α ⊕ β)
⊢ s✝ ∈ 𝓝 x ↔ s✝ ∈ comap (Prod.mk x) (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β))
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝³ : UniformSpace β
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : DiscreteTopology α
inst✝ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ IsClosedEmbedding f

Tactic:
rcases @DiscreteTopology.eq_bot α _ _ with rfl

Goal state after:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
inst✝ : DiscreteTopology α
⊢ IsClosedEmbedding f
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ CompleteSpace α ↔ IsComplete (range f)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
constructor

Goal state after:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
by
    constructor
    · intro H
      have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
      obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
      exact ⟨i, hpi, hi.trans interior_subset⟩
    · rintro ⟨i, hpi, hi⟩
      refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi
      exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
obtain ⟨t, ht, hst⟩ := h (SetRel.inv U)
      (mem_of_superset (symmetrize_mem_uniformity hU) SetRel.symmetrize_subset_inv)
    exact ⟨t, ht.countable, hst⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s✝ : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s✝ x
hg : Tendsto g p (𝓝[s✝] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s✝] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s✝] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
B : ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁
⊢ u₀ ∈ map (fun x_1 ↦ (f x, F x_1 (g x_1))) p

Tactic:
exact B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ <| prodMk_mem_comp H3 <| H1 _ H2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

case mpr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ (∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
by
  simp only [UniformEquicontinuous, eventually_all, @forall_comm _ ι]; rfl

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ EquicontinuousWithinAt F S x₀ → ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

case mpr
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) → EquicontinuousWithinAt F S x₀
Module: Mathlib.Topology.Algebra.Monoid.Defs

Goal state before:
pp: α : Type u_2
E : Type u_3
inst✝² : CommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f g : α → E
m : E
x : Filter α
hf : Tendsto f x (𝓝 m)
hfg : Tendsto (g / f) x (𝓝 1)
⊢ Tendsto g x (𝓝 m)

Tactic:
by
  simpa using Tendsto.mul hf hfg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsUniformInducing ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (fun x ↦
        ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ) x.1,
          (Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ) x.2))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
huf : Tendsto id u (𝓝 f)
⊢ f ∈ {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}

Tactic:
UniformFun.tendsto_iff_tendstoUniformly

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
huf : TendstoUniformly (⇑toFun ∘ id) (toFun f) u
⊢ f ∈ {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) S x₀

Tactic:
intro U hU
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS
  rw [SetCoe.forall] at *
  change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx
  refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)
  exact (continuous_apply ⟨x, hxS⟩).comp hu₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ IsUniformInducing (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
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 γ
⊢ IsUniformInducing
    ⇑((ofFun 𝔖).symm.trans
        ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))

Tactic:
constructor

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 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: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)

case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case mp
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * y ∈ Icc (a * b) (a * c)

Tactic:
constructor

Goal state after:
case mp.left
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * b ≤ a * y

case mp.right
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * y ≤ a * 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 α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing ⇑(Equiv.piComm fun a ↦ δ)

Tactic:
constructor

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)
⊢ comap (fun x ↦ ((Equiv.piComm fun a ↦ δ) x.1, (Equiv.piComm fun a ↦ δ) x.2)) (𝓤 ((i : ι) → α →ᵤ[𝔖] δ i)) =
    𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
by
  simpa using neBot_iff.mp h

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
⊢ (fun x ↦ x + b) '' (fun x ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Icc' h, image_add_const_Icc]

Goal state after:
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
⊢ U = (fun m' ↦ m' * m⁻¹) ⁻¹' ↑(MulAction.stabilizer M x)

Tactic:
ext

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
x✝ : M
⊢ x✝ ∈ U ↔ x✝ ∈ (fun m' ↦ m' * m⁻¹) ⁻¹' ↑(MulAction.stabilizer M x)
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
⊢ (fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝) = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
a✝ : α
⊢ ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝)) a✝ = x✝ a✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : α → β
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝) = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝¹ : α → β
x✝ : α
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
a✝ : ↑(S i)
⊢ (restrict (S i) (liftCover S φ hφ hS)) a✝ = (φ i) a✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: case e'_5
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
⊢ (Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f = Quotient.mk'

Tactic:
ext

Goal state after:
case e'_5
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
x✝ : X
⊢ ((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f) x✝ = Quotient.mk' x✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
⊢ (hf.lift g h).comp f = g

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ ((hf.lift g h).comp f) a✝ = g a✝
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
⊢ (fun x ↦ c • x) ∘ ⇑f = ⇑f ∘ fun x ↦ (c • 1) • x

Tactic:
ext

Goal state after:
M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
x✝ : α
⊢ ((fun x ↦ c • x) ∘ ⇑f) x✝ = (⇑f ∘ fun x ↦ (c • 1) • x) x✝