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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
x y : ConnectedComponents α
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := surjective_coe x

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
y : ConnectedComponents α
x : α
⊢ mk x = y
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsConnected (U i)
i : ι
x : α
hx : x ∈ U i
⊢ (equivOfIsClopenOfIsConnected hclopen hdisj hunion hconn) (mk x) = i

Tactic:
simp [equivOfIsClopenOfIsConnected, equivOfIsClopen_mk _ _ _ _ hx]

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
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ Continuous[inst✝², inst✝³] ⇑f.symm

Tactic:
rw [continuous_iff_isClosed]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ ∀ (s : Set X), IsClosed[inst✝³] s → IsClosed[inst✝²] (⇑f.symm ⁻¹' s)
Module: Mathlib.Topology.Homeomorph.Lemmas

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

Tactic:
refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
  · let h := hf.homeomorph f
    exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
  · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

Goal state after:
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:
nhds_nhds_eq_uniformity_uniformity_prod,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}) =
    (𝓤 α).lift' fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩

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

Goal state before:
pp: case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SetRel.IsSymm V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, V_in, V_sub⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 {x}) (𝓤 β) ↔ Tendsto (fun n ↦ F n x) p (𝓝 (f x))

Tactic:
Uniform.tendsto_nhds_right,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 {x}) (𝓤 β) ↔ Tendsto (fun x_1 ↦ (f x, F x_1 x)) p (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q ↦ ((x, q.2), q)
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
exact tendsto_comap.prodMk (tendsto_diag_uniformity _ _)

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f = pure x

Tactic:
rcases hf with ⟨f_ne_bot, f_le⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : f ×ˢ f ≤ 𝓤 α
⊢ ∃ x, f = pure x
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
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ l') (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ 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
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ l', (f x.2, F x.1 x.2) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
rw [ContinuousWithinAt, tendsto_nhds_left]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set α
⊢ CompleteSpace ↑s ↔ IsComplete s

Tactic:
rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
    Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
i : ι
p4 : (L i, ℓ) ∈ t
p5 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p6 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩

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 : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
choose U hU using h V hV

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib

Tactic:
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ (x : α), (toFun f x, (⇑toFun ∘ F) n x) ∈ u

Tactic:
simp only [mem_ofPred, UniformFun.gen, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
UniformOnFun.uniformity_eq_of_basis _ _ h,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Tactic:
map₂_swap m',

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ (fun a b ↦ m' b a) h f)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

Goal state after:
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
⊢ f = pure a

Tactic:
rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]

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 = (Ioo 0 a⁻¹)⁻¹

Tactic:
inv_Ioo_0_left (inv_pos.2 ha),

Goal state after:
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⁻¹⁻¹
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 : IsOpen[inst✝⁵] U
⊢ IsOpen[inst✝⁵] ((fun x ↦ (x, y).1 • (x, y).2) ⁻¹' {x})

Tactic:
simpa using! hU

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

Goal state before:
pp: G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
s : Set X
hs : s ∈ 𝓝 0
x : X
this : Tendsto (fun x_1 ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc : c ∈ (fun x_1 ↦ x_1 • x) ⁻¹' s
hc₀ : ¬c = 0
⊢ ∃ x_1, ∃ y ∈ s, x_1 • y = x

Tactic:
exact ⟨c⁻¹, c • x, hc, inv_smul_smul₀ hc₀ _⟩

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

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : SMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
x : T
⊢ {γ | γ • x = x}.Finite

Tactic:
by
  simp_rw [← mem_singleton_iff, ← singleton_inter_nonempty, ← image_singleton]
  exact finite_disjoint_inter_image isCompact_singleton isCompact_singleton

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_

Goal state after:
case refine_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∅ * V ⊆ U

case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ Tendsto g (↑(Ultrafilter.map snd 𝒰)) (𝓝 w)

Tactic:
simpa using! hyw.2

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
s t : Set G
ht : IsOpen[inst✝²] t
⊢ IsOpen[inst✝²] (s / t)

Tactic:
by
  rw [← iUnion_div_left_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Goal state after:
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:
rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap, Function.comp_def]

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

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (fun x_1 ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y

Tactic:
exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

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

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ x / c) (𝓝[≠] a) = 𝓝[≠] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [div_eq_mul_inv]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_

Goal state after:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U

case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: α : Type u
inst✝ : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Tactic:
cases f
    cases g
    congr

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

Goal state before:
pp: R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 * p.2

Tactic:
by
    refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_ <;>
      simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : Prod.map (⇑e) (⇑f) z = x
⊢ ∃ a, Prod.map (⇑e) (⇑f) a ∈ U

Tactic:
exists z

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : Prod.map (⇑e) (⇑f) z = x
⊢ Prod.map (⇑e) (⇑f) z ∈ U
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) = ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | a / a_1 < x}

pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | x⁻¹ < a / a_1}

Tactic:
· refine (Equiv.divLeft a).iInf_congr fun x => ?_; simp [Ioi]

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | x⁻¹ < a / a_1}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[ts] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
rw [t.topology_eq_generate_intervals]

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
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:
by
  mfld_set_tac

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₃

Tactic:
have := hS.epi_g
  exact P.prop_of_epi S.g h₂

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
hy : n • y = ↑(f x) • p
y' : 𝕜
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'

Tactic:
eq,

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
hy : n • y = ↑(f x') • p
y' : 𝕜
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
⊢ atTop.IsCountablyGenerated

Tactic:
obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
⊢ atTop.IsCountablyGenerated

case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ atTop.IsCountablyGenerated
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
⊢ ∃ m < addOrderOf ↑k, m.gcd (addOrderOf ↑k) = 1 ∧ ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k

Tactic:
obtain ⟨m, hm, hk⟩ := (AddCircle.nsmul_eq_zero_iff h).mp
    (addOrderOf_nsmul_eq_zero (k : AddCircle p))

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ ∃ m < addOrderOf ↑k, m.gcd (addOrderOf ↑k) = 1 ∧ ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k