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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
by
  by_cases hx : x ∈ F
  · rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
      show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]
    exact image_mono ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)
  · rw [connectedComponentIn_eq_empty hx]
    exact Set.empty_subset _

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α

Tactic:
rintro ⟨x, h⟩

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
by
  have : IsLindelof (⋃ i, U i) := HereditarilyLindelofSpace.isLindelof (⋃ i, U i)
  rcases this.elim_countable_subcover U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩
  use t, htc
  apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu

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

Goal state before:
pp: case inl
α : 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)
x✝ : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ ∅.Subsingleton

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:
· exact subsingleton_empty

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)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
⊢ s.Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s_sub : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ ∅.Subsingleton

pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
· exact subsingleton_empty

Goal state after:
case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n) → IsGδ s

Tactic:
· rintro ⟨T, hT, T_count, rfl⟩
    rcases Set.eq_empty_or_nonempty T with rfl | hT
    · exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
    · obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
      exact ⟨f, by simp_all, by simp [hf]⟩

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n) → IsGδ s
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
⊢ Dense (⋂ n, f n)

Tactic:
let c := fun n : ℕ => p '' f n ∪ (closure s)ᶜ

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
⊢ Dense (⋂ n, f n)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
⊢ BaireSpace Y

Tactic:
by
  constructor
  intro f hof hdf
  let s := range p
  let c := fun n : ℕ => p '' f n ∪ (closure s)ᶜ
  have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
    isClosed_closure.isOpen_compl
  have c_dense (n : ℕ) : Dense (c n) := by
    rw [dense_iff_closure_eq, subset_antisymm_iff]
    have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
    grind
  have c_inter_dense : Dense (⋂ n, c n) := dense_iInter_of_isOpen_nat c_open c_dense
  have c_inter_eq : ⋂ n, f n = p ⁻¹' (⋂ n, c n) := by
    ext x
    simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
    refine ⟨fun h i => by grind, fun h i => ?_⟩
    exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))
  exact c_inter_eq ▸ Dense.preimage c_inter_dense hp.isOpenMap

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

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ v

Tactic:
· refine Subset.trans ?_ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

Goal state after:
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
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V

Tactic:
set φ := fun q : α × β => ((x, q.2), q)

Goal state after:
α : 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)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓟 (s ×ˢ s)) (𝓟 (t ×ˢ t))

Tactic:
simp only [tendsto_principal, mem_prod, eventually_principal, and_imp, Prod.forall]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case h
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
i : ι
⊢ f i ≤ 𝓟 (U.preimage (t i))

Tactic:
apply ht

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f g : Filter α
⊢ (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded

Tactic:
rw [sup_eq_iSup, totallyBounded_iSup]
  simp [and_comm]

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

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ d.preimage t ∈ g

Tactic:
contrapose! H with hd_cover

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
⊢ ∃ f, f.NeBot ∧ f ≤ g ∧ ∀ c ≤ f, ¬Cauchy c
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

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

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

Tactic:
simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
c : γ
hc : Tendsto (fun x ↦ f ↑x) (comap (IsDenseEmbedding.subtypeEmb p e) (𝓝 ⟨b, this⟩)) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
    simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using! hc

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists

Goal state after:
α : 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
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:
by
  rw [sUnion_eq_iUnion] at hcover
  simpa using lebesgue_number_lemma hK (by simpa) hcover

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ⇑f
x : β
⊢ f.symm (f (g x)) = f.symm x

Tactic:
by rw [hg x]

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

Tactic:
by
  refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_
  obtain hxbc | hbcx := le_total x (b * c)
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hacx
    refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩
    rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hbcx
    refine ⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxbd

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

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a b : α
⊢ Ici a * Ici b = Ici (a * b)

Tactic:
refine Subset.antisymm (Ici_mul_Ici_subset' ..) (subset_def ▸ fun c c_in ↦
    mem_mul.mpr ⟨a, ⟨by simp, ?_⟩⟩)
  obtain ⟨d, hd⟩ := exists_mul_of_le <| mem_Ici.mp c_in
  exact ⟨b * d, by simp [← mul_assoc, hd]⟩

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

Goal state before:
pp: case neg
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
h' : γ • x ∈ L₀
H : γ • K₀ ∩ L₀ = ∅
⊢ False

Tactic:
exact eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ

Tactic:
rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
x : X
hxy : f x = y
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
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
hg : IsProperMap g
hf : IsProperMap f
⊢ IsProperMap (g ∘ f)

Tactic:
refine ⟨by fun_prop, fun ℱ z h ↦ ?_⟩

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
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z ℱ (g ∘ f)
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
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 : M
hx : x ∈ K
this : U ∈ map (fun p ↦ p.1 * p.2) (𝓝 (x, 0))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this

Goal state after:
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 : M
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
have K_compact : IsCompact K := .prod (hf.isCompact_insert_range_of_cocompact f_cont)
    (hg.isCompact_insert_range_of_cocompact g_cont)

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
rw [← sInf_range]
  exact continuousInv_sInf (Set.forall_mem_range.mpr h')

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
x y : G
⊢ Inseparable x y ↔ x / y ∈ closure[inst✝²] 1

Tactic:
rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable,
    ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]
  simp [div_eq_mul_inv]

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
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ LocallyCompactSpace G

Tactic:
suffices WeaklyLocallyCompactSpace G from inferInstance

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ WeaklyLocallyCompactSpace G
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ Tendsto f l atBot

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
by
  simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]

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

Goal state before:
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 : G
hx : x ∈ K
this : U ∈ map (fun p ↦ p.1 * p.2) (𝓝 (x, 1))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this

Goal state after:
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 : G
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_pos h]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
s : Set α
⊢ (∀ i ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ {x | x.2⁻¹ * x.1 ∈ id i}}) ↔
    ∀ U ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

Tactic:
by
    simp [← preimage_smul_inv, preimage]

Goal state after: