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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Tactic:
exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩

Goal state after:
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id
⊢ ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
U

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
⊢ U ∈ 𝓝 x✝ → ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V) →
    (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id

Tactic:
· exact fun h => ⟨fun U => ⟨fun hU =>
      let ⟨V, hVU, hV⟩ := h U hU
      ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h

Tactic:
by
  simp only [biUnion_eq_iUnion]
  have := hS.toEncodable
  exact EventuallyLE.countable_iUnion fun i => h i i.2

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Goal state after:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
⊢ ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
U

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
⊢ U ∈ 𝓝 x → ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V) →
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
intro h x U hxU

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter ⊤

Tactic:
by
  rw [← principal_univ]
  apply countableInterFilter_principal

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.empty
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑∅
⊢ ∃ u ∈ ∅, s ⊆ u

Tactic:
exact absurd (by simpa using hsU) hne.not_subset_empty

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
⊢ ∀ (U : i → Set X),
    (∀ (i : i), IsOpen[inst✝] (U i)) → ⋃ i ∈ s, f i ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1

Tactic:
U

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
⊢ (∀ (i : i), IsOpen[inst✝] (U i)) → ⋃ i ∈ s, f i ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
ι✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
ι : Type u
⊢ ∀ (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝²] (U i)) → t ⊆ ⋃ i, U i → ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i

Tactic:
U

Goal state after:
X : Type u
Y : Type v
ι✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
ι : Type u
U : ι → Set X
⊢ (∀ (i : ι), IsOpen[inst✝²] (U i)) → t ⊆ ⋃ i, U i → ∃ t_1, t_1.Countable ∧ t ⊆ ⋃ i ∈ t_1, U i
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
by
  constructor
  · intro h x
    apply h.1
    · exact subset_univ _
    exact isPreconnected_connectedComponent
  intro h; constructor
  intro s s_sub hs
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
  · exact subsingleton_empty
  · exact (h x).anti (hs.subset_connectedComponent x_in)

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = ⇑h '' {x}ᶜ

Tactic:
rw [h.image_compl, Set.image_singleton]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst✝, inst✝¹] g
hf : Continuous[inst✝¹, inst✝] f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst✝, inst✝¹] g
⊢ IsHomeomorph f

Tactic:
exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

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

Goal state before:
pp: case hopen
α : Type u
u : Core α
x a : α
⊢ ∀ i ∈ u.uniformity, ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity

Tactic:
U

Goal state after:
case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
⊢ U ∈ u.uniformity → ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

Tactic:
have : ∀ n, ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n := fun n => by
    rw [cauchySeq_iff] at hu
    rcases hu _ (hV n) with ⟨N, H⟩
    exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
hβ.tendsto_right_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs : s ∈ map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p ↦ (inl p.1, inl p.2)) ⁻¹' s
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p ↦ (inr p.1, inr p.2)) ⁻¹' s
⊢ s ∈ (map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)).lift' fun s ↦ s ○ s

Tactic:
filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs : s ∈ map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p ↦ (inl p.1, inl p.2)) ⁻¹' s
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p ↦ (inr p.1, inr p.2)) ⁻¹' s
⊢ ∀
    a ∈
      (fun p ↦ (inl p.1, inl p.2)) '' tα ∪ (fun p ↦ (inr p.1, inr p.2)) '' tβ ○
        (fun p ↦ (inl p.1, inl p.2)) '' tα ∪ (fun p ↦ (inr p.1, inr p.2)) '' tβ,
    a ∈ s
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformly (fun n ↦ F n ∘ g) (f ∘ g) p

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
  rw [← continuousOn_univ] at cg
  exact h.comp _ (mapsTo_univ _ _) cg

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

Goal state before:
pp: 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
H : EquicontinuousWithinAt F S x₀
⊢ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
U

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
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: 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
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ EquicontinuousWithinAt F S x₀

Tactic:
U

Goal state after:
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
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
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
⊢ EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀

Tactic:
by
  rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
  rfl

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i →
      {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i} ∈ F

Tactic:
U

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
⊢ U ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] U →
    {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id U} ∈ F
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 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:
rw [uniformity_prod, comap_inf, comap_comap, comap_comap]

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.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 + 1)

Tactic:
pow_succ

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: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one
    have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
    rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
    obtain ⟨a, b, rfl, rfl, h⟩ := h
    refine ⟨a, b, ?_, ?_, h⟩
    · rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
    · rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
x : ↑s
hf : ContinuousOn f s
⊢ (mkD (s.domRestrict f) g) x = f ↑x

Tactic:
rw [mkD_of_continuousOn hf, coe_mk, Set.domRestrict_apply]

Goal state after:
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
⊢ LeftInverse (fun g ↦ ⟨g.comp f, ⋯⟩) fun g ↦ hf.lift ↑g ⋯

Tactic:
by intro; simp

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous[inst✝¹, inst✝] f
f_inj : Injective f
⊢ IsProperMap f ↔ IsClosedMap f

Tactic:
refine ⟨fun h ↦ h.isClosedMap, fun h ↦ ?_⟩
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  exact ⟨f_cont, h, fun y ↦ (subsingleton_singleton.preimage f_inj).isCompact⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space (G ⧸ N) ↔ IsClosed[inst✝²] ↑N

Tactic:
rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
      isClosed_coinduced]
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed[inst✝²] W
hW : W ⊆ V
⊢ (W ∩ W⁻¹)⁻¹ = W ∩ W⁻¹

Tactic:
by simp [inter_comm]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
⊢ IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
hL

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ (fun x ↦ (x.1 * a, x.2 * a)) (p₁, p₂) = (fun x ↦ (x.1 * a, x.2 * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)

Tactic:
simp only [Prod.mk.injEq, mul_left_inj, imp_self]

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
x y : α
⊢ IsLUB (f '' {x, y}) (f x ⊔ f y)

Tactic:
simp only [image_pair, isLUB_pair]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
c d : 𝕜
⊢ Tendsto (fun x ↦ c * x ^ 0) atTop (𝓝 d) ↔ (c = 0 ∨ 0 = 0) ∧ c = d

pp: case inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
· simp [tendsto_const_nhds_iff]

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inr.inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d

pp: case inr.inr.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
· simp [tendsto_const_nhds_iff]

Goal state after:
case inr.inr.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_1.negSucc
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0

Tactic:
exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)

Tactic:
mfld_set_tac

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans e.symm).source = e.source

Tactic:
mfld_set_tac

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
by
  have A : (e.trans e.symm).source = e.source := by mfld_set_tac
  refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩
  rw [A] at hx
  simp only [hx, mfld_simps]

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

Goal state before:
pp: case a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ generateFrom {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ generateFrom t

Tactic:
apply generateFrom_anti

Goal state after:
case a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ t ⊆ {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoDiv hp a =ᶠ[𝓝 x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
rw [← nhdsLT_sup_nhdsGE, Filter.EventuallyEq, Filter.eventually_sup]
  refine ⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩
  convert! (eventuallyEq_toIcoDiv_nhdsLT hp a x).eventually using 3
  rwa [← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Mono f
hN : N.isFinite
⊢ M.isFinite

Tactic:
AddCommGrpCat.mono_iff_injective

Goal state after:
M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hN : N.isFinite
⊢ M.isFinite
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
constructor
  · intro h
    rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
    rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
    exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
  · rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: n : ℕ
⊢ (int.divByNat n) ↑n = 0

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Goal state after:
case inl
⊢ (int.divByNat 0) ↑0 = 0

case inr
n : ℕ
h0 : n ≠ 0
⊢ (int.divByNat n) ↑n = 0