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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
z : α
hz : z ∈ u
t : α
⊢ P z t ∧ P t z → t ∈ u

Tactic:
ht

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
z : α
hz : z ∈ u
t : α
ht : P z t ∧ P t z
⊢ t ∈ u
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
⊢ P x y

Tactic:
have B : IsOpen u := by
    apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
    filter_upwards [h z] with t ht
    exact h'.trans x z t hz ht.1

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
B : IsOpen[inst✝¹] u
⊢ P x y
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
⊢ t.Countable → ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
ht

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
⊢ ¬s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (univ.pi s).Nonempty → (IsPreconnected (univ.pi s) ↔ ∀ (x : ι), IsPreconnected (s x))

Tactic:
refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected (s i)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
⊢ CompletelyNormalSpace X

Tactic:
by
  refine ⟨fun s t hd₁ hd₂ => ?_⟩
  simp only [he.nhdsSet_eq_comap]
  refine disjoint_comap (completely_normal ?_ ?_)
  · rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
  · rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set X
⊢ IsLindelof t → ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
ht

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set X
ht : IsLindelof t
⊢ ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case inr
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s✝ t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
⊢ s.Subsingleton

Tactic:
obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩

Goal state after:
case inr
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t✝ u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
a : ι
t : Set (X a)
ht : IsConnected t
x✝ : Sigma.mk a '' t ⊆ univ
hs : IsPreconnected (Sigma.mk a '' t)
h : (Sigma.mk a '' t).Nonempty
⊢ (Sigma.mk a '' t).Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
⊢ IsPreconnected t → t.Subsingleton

Tactic:
ht

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
⊢ t.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst✝¹, inst✝] f
U : ℕ → Set Y
hs : IsGδ (⋂ n, U n)
hU1 : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hU2 : s = ⋂ n, U n
⊢ IsGδ (⋂ i, f ⁻¹' U i)

Tactic:
exact IsGδ.iInter_of_isOpen (fun i => hf.isOpen_preimage (U i) (hU1 i))

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] t) ⊆ ∅

Tactic:
ht

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] s) ⊆ ∅
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      (∀ t ∈ compl '' x, IsOpen[inst✝] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
simp_rw [← and_assoc, ← forall_and, forall_mem_image, ← isClosed_isNowhereDense_iff_compl,
    sInter_image, ← compl_iUnion₂, compl_subset_compl, ← sUnion_eq_biUnion, and_assoc]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)

Goal state after:
case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
i : Fin (n + 1)
hi : ¬IsConnected (U i)
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ univ.Nonempty ∧ IsPreconnected univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
← preconnectedSpace_iff_univ,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ univ.Nonempty ∧ PreconnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Tactic:
simp [TendstoUniformlyOn, TendstoUniformly]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id
⊢ ∃ x, f = pure x

Tactic:
obtain ⟨S, hS, T, hT, H⟩ := f_le

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
S : Set α
hS : S ∈ f
T : Set α
hT : T ∈ f
H : S ×ˢ T ⊆ SetRel.id
⊢ ∃ x, f = pure x
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ (i : ι), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity, tendsto_iInf]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
h : ∀ V ∈ 𝓤 α, SetRel.IsSymm V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y V
V : SetRel α α
x✝ : V ∈ 𝓤 α ∧ V.IsSymm
left✝ : V ∈ 𝓤 α
right✝ : V.IsSymm
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ id V}

Tactic:
by
    simpa only [ball_eq_of_symmetry] using! h V ‹_› ‹_›

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 β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.30

Tactic:
exact UniformContinuous fun p : α × β => f p.1 p.2

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 β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.31

Tactic:
exact UniformContinuous fun p : α × β => f p.1 p.2

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
⊢ t ∈ 𝓤 β → ∃ t_1, t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F

Tactic:
ht

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
⊢ ∃ t_1, t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst✝.toTopologicalSpace] s
hcover : K ⊆ ⋃₀ S
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Tactic:
rw [sUnion_eq_iUnion] at hcover
  simpa using lebesgue_number_lemma hK (by simpa) hcover

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

Goal state before:
pp: X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ closure[inst✝¹] (mulSupport (g ∘ f)) = closure[inst✝¹] (mulSupport f)

Tactic:
mulSupport_comp_eq_of_range_subset hg

Goal state after:
X : Type u_1
α : Type u_2
β : Type u_4
inst✝² : One α
inst✝¹ : TopologicalSpace X
inst✝ : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ closure[inst✝¹] (mulSupport f) = closure[inst✝¹] (mulSupport f)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : f.NeBot
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
cauchy_pi_iff',

Goal state after:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
hf : ∀ (i : ι), Cauchy (map (eval i) f)
⊢ ∃ x, f ≤ 𝓝 x
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 : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

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
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
· rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
    refine ⟨_, H V hV, fun x hx y hy i => hVU (SetRel.prodMk_mem_comp ?_ (hy i))⟩
    exact SetRel.symm V (hx i)

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 (α × α)
hU : 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
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F S x₀
⊢ EquicontinuousWithinAt F S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢
  unfold ContinuousWithinAt nhdsWithin at hk ⊢
  rw [nhds_iInf]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i ↦ UniformOnFun.gen 𝔖 S (s i)

Tactic:
UniformOnFun.gen_eq_preimage_restrict,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i ↦
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map (fun p ↦ m p.1 p.2) (pure a ×ˢ g) = map (m a) g

Tactic:
pure_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map (fun p ↦ m p.1 p.2) (map (Prod.mk a) g) = map (m a) g
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:
exact u.inv_mul

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✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iic, h]

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

Goal state before:
pp: G₀ : Type u_2
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
h : 0 < c
⊢ (fun x ↦ c * x) ⁻¹' Icc a b = Icc (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iic, h]

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

Goal state before:
pp: G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
⊢ IsClosedMap fun x ↦ c • x

Tactic:
rcases eq_or_ne c 0 with (rfl | hne)
  · simp only [zero_smul]
    exact isClosedMap_const
  · exact (Homeomorph.smulOfNeZero c hne).isClosedMap

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

Goal state before:
pp: M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n : ℕ
⊢ (a ^ Nat.zero) ⤳ (b ^ Nat.zero)

Tactic:
simp only [pow_zero, specializes_rfl]

Goal state after:
Module: Mathlib.Topology.Maps.Proper.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 : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 ℱ

Tactic:
← ℱ.map_comap_of_surjective f_surj

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 : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))
Module: Mathlib.Topology.Maps.Proper.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 : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter_of_t2]
  refine ⟨hf, fun 𝒰 y h ↦ ?_⟩
  rw [isProperMap_iff_ultrafilter] at hgf
  rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩
  exact ⟨x, hx⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen[inst✝²] V ∧ 1 ∈ V ∧ V * V ⊆ U

Tactic:
by
  simpa only [mul_subset_iff] using exists_open_nhds_one_split hU

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

Goal state before:
pp: ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x

Tactic:
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ ∀ t ∈ range fun i ↦ {x | i ∈ s → i * x = x * i}, IsClosed[inst✝²] t

Tactic:
rintro - ⟨m, ht, rfl⟩

Goal state after:
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ IsClosed[inst✝²] ((fun i ↦ {x | i ∈ s → i * x = x * i}) m)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
⊢ IsClosed[inst✝⁵] t → IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)

Tactic:
ht

Goal state after:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed[inst✝⁵] t
⊢ IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
⊢ IsClosed[inst✝²] t → IsClosed[instTopologicalSpace H] (mk '' t)

Tactic:
ht

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed[inst✝²] t
⊢ IsClosed[instTopologicalSpace H] (mk '' t)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)

Tactic:
← comap_swap_uniformity,

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap Prod.swap (𝓤 Gᵣ) = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure[inst✝²] {1}
⊢ False

Tactic:
ht

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
← comap_swap_uniformity,

Goal state after:
Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ comap Prod.swap (𝓤 Gₗ) = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.1 / x.2) (𝓝 1)

Tactic:
← comap_swap_uniformity,

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap Prod.swap (𝓤 Gᵣ) = comap (fun x ↦ x.1 / x.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))
hr : ∀ (y : H), Tendsto (fun x ↦ (f x) y) (𝓝 1) (𝓝 ((f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x ↦ (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ 𝓝 ((f x) y * (f 1) y * ((f x) 1 * (f 1) 1)) = 𝓝 ((f x) y)

Tactic:
simp only [map_one, mul_one, MonoidHom.one_apply]

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Tactic:
by
  have hmaps : MapsTo f S {1, -1} := by
    simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using! hsq
  simpa using! hS.eqOn_const_of_mapsTo (toFinite _).isDiscrete hf hmaps

Goal state after: