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

Goal state before:
pp: α : 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)
⊢ TotallyDisconnectedSpace ((i : ι) × X i)

Tactic:
by
  refine ⟨fun s _ hs => ?_⟩
  obtain rfl | h := s.eq_empty_or_nonempty
  · exact subsingleton_empty
  · obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
    exact ht.isPreconnected.subsingleton.image _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
rcases fiber_decomp t' ht' with htu | htv

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁ ∨ t' ∈ T₂

case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₁ ∨ t' ∈ T₂
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
by
  suffices IsMeagre (⋃ i : I, f i) by simpa
  have : Countable I := c
  apply isMeagre_iUnion
  intro ⟨i, hi⟩
  exact h i hi

Goal state after:
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
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

Tactic:
intro u ⟨t, tT, tu⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
⊢ IsNowhereDense u
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:
h.image_compl,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = (⇑h '' {x})ᶜ
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inl s)

Tactic:
dsimp

Goal state after:
case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ a.1 s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inr t)

Tactic:
dsimp

Goal state after:
case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ a.2 t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
by
  simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]

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:
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 α
s : Set α
x : α
⊢ x ∈ closure[inst✝.toTopologicalSpace] s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (s ∩ ball x V).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
⊢ t ∈ (map (Prod.map mk mk) (𝓤 α)).lift' fun s ↦ SetRel.comp s s

Tactic:
rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
⊢ t ∈ (map (Prod.map mk mk) (𝓤 α)).lift' fun s ↦ SetRel.comp s s
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ UniformContinuous f ↔ UniformContinuous fun p ↦ f (mk p.1, mk p.2)

Tactic:
simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq,
    tendsto_map'_iff]
  rfl

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
⊢ CompleteSpace α

Tactic:
by
  obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
  have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
  refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
  · exact inter_subset_left (seq_pair_mem hf Hmem hm hn)
  · rcases hU'.1 hs with ⟨N, hN⟩
    exact ⟨N, Subset.trans inter_subset_right hN⟩

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

Goal state before:
pp: α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ (Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α)).HasBasis (fun U ↦ U ∈ 𝓤 α) fun U ↦
    (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
exact (𝓤 α).basis_sets.prod_self.comap _

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

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
this✝ : IsUniformInducing (const ι)
this : Pi.topologicalSpace ≤ Pi.topologicalSpace
⊢ IsClosed[Pi.topologicalSpace] (⋂ i, ⋂ i_1, {x | x i = x i_1})

Tactic:
exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

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 ι
h : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝¹ : α
x✝ : x✝¹ ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u

Tactic:
by simpa using h u hu

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 ι
h : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝ : α
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ univ, (f y, F n y) ∈ u

Tactic:
by simpa using h u hu

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, (∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s) ∧ ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
F : α → β
hF : ∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s
hFv : ∀ y ∈ s, (f y, F y) ∈ v
⊢ {x | (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u} ∈ 𝓤 ↑s

Tactic:
filter_upwards [hF v hv] with x hx

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, (∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s) ∧ ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
F : α → β
hF : ∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s
hFv : ∀ y ∈ s, (f y, F y) ∈ v
x : ↑s × ↑s
hx : (s.domRestrict F x.1, s.domRestrict F x.2) ∈ v
⊢ (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u
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
⊢ (fun x ↦ a • x) y ∈ Icc (a * b) (a * c)

Tactic:
dsimp

Goal state after:
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)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1

Tactic:
rintro ⟨a, b, rfl, rfl, h⟩

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1
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, β)
hf : ¬ContinuousOn f s
⊢ mkD (s.domRestrict f) g = g

Tactic:
rw [continuousOn_iff_continuous_domRestrict] at hf
  exact mkD_of_not_continuous hf

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

Goal state before:
pp: 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

pp: 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

pp: 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

Tactic:
· rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩

Goal state after:
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.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i ↦ f i x) ⊆ ↑I

Tactic:
refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩

Goal state after:
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ ↑hUf.toFinset
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ connectedComponent g = {g}

Tactic:
by
      rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)

Tactic:
congrm Tendsto ?_ _ _

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ id = (Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) 𝓕 (𝓤 α)

Tactic:
congrm Tendsto ?_ _ _

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ id = (fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (f x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ C * g x) x✝¹

Tactic:
dsimp

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (f x✝¹) C
⊢ f x✝¹ * g x✝¹ ≤ C * g x✝¹
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (g x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ f x * C) x✝¹

Tactic:
dsimp

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (g x✝¹) C
⊢ f x✝¹ * g x✝¹ ≤ f x✝¹ * C
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: 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

pp: 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

pp: 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

Tactic:
· rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩

Goal state after:
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.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
⊢ SigmaCompactSpace G

Tactic:
by
  obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
  refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
  · intro n
    exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc
  · refine iUnion_eq_univ_iff.2 fun x => ?_
    obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty := by
      rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
      exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
    exact ⟨n, hn⟩

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
⊢ ∃ x, ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
by
      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
      exact hf.eventually_mem K_mem |>.curry.exists

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

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun

Tactic:
simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap]

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

Goal state before:
pp: F✝ : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : TopologicalSpace D
F : Type u_7
inst✝² : FunLike F A B
inst✝¹ : MonoidHomClass F A B
inst✝ : ContinuousMapClass F A B
f : F
⊢ Continuous[inst✝⁶, inst✝⁵] (↑↑f).toFun

Tactic:
dsimp

Goal state after:
F✝ : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : TopologicalSpace D
F : Type u_7
inst✝² : FunLike F A B
inst✝¹ : MonoidHomClass F A B
inst✝ : ContinuousMapClass F A B
f : F
⊢ Continuous[inst✝⁶, inst✝⁵] ⇑f
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous (MulEquiv.refl M).toFun

Tactic:
dsimp

Goal state after:
G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous id
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous (MulEquiv.refl M).invFun

Tactic:
dsimp

Goal state after:
G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous id
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_2
𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x

Tactic:
· filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
    exact inv_lt_of_inv_lt₀ (by positivity) hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

Tactic:
rw [← h.image_eq]
  rintro y ⟨x, hx, rfl⟩
  have hx' := hx; rw [hs] at hx'
  rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]

Goal state after: