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

Goal state before:
pp: case a
α : 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₂ : Set β := ⋯
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ∩ (u ∩ v) = ∅

Tactic:
rw [uv_disj.inter_eq, inter_empty]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
⊢ IsLindelof s

Tactic:
by tauto

Goal state after:
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
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ∪ (interior (closure[inst✝²] s))ᶜ ⊆ closure[inst✝²] s ∪ (interior (closure[inst✝²] s))ᶜ

Tactic:
gcongr

Goal state after:
case h₁
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 := ⋯
c : ℕ → Set X := ⋯
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ⊆ closure[inst✝²] s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ w ○ w

Tactic:
gcongr

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ w ○ (t ○ t)

Tactic:
gcongr

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ w ○ (t ○ t) ⊆ w ○ w

Tactic:
gcongr

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (s.image t)

Tactic:
SetRel.image,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] {b | ∃ a ∈ t, (a, b) ∈ s}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] (s.image t)

Tactic:
SetRel.image,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] {b | ∃ a ∈ t, (a, b) ∈ s}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
t : SetRel α α
x✝¹ x✝ : Set (α × α)
hV : x✝¹ ⊆ x✝
⊢ x✝¹ ○ t ○ x✝¹ ⊆ x✝ ○ t ○ x✝

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t

Tactic:
gcongr

Goal state after:
case hs
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t

case ht
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋯
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_3
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
⊢ U.preimage (range g) ∈ f

Tactic:
filter_upwards [hs, ks] with x xs ⟨y, hy, xy⟩
    simp_rw [SetRel.preimage, exists_range_iff]
    set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩
    exact ⟨z, rU ⟨y, xy, rs (hgr z)⟩⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
U : ι → SetRel α α
H : (𝓤 α).HasBasis p U
f : Filter α
x✝³ x✝² : Set (α × α)
x✝¹ : x✝³ ⊆ x✝²
h : ∃ t, t.Finite ∧ SetRel.preimage x✝³ t ∈ f
x✝ : Set α
ht : x✝.Finite ∧ SetRel.preimage x✝³ x✝ ∈ f
⊢ SetRel.preimage x✝³ x✝ ⊆ SetRel.preimage x✝² x✝

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
rw [h.prod rfl]
  apply nhds_le_uniformity

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

Goal state before:
pp: α : 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 ≤ ⨆ x, 𝓟 (U.preimage (t x))

Tactic:
gcongr

Goal state after:
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))
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
⊢ g.TotallyBounded

Tactic:
d

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
s t : Finset α
h : s ⊆ t
⊢ g ⊓ 𝓟 (d.preimage ↑t)ᶜ ≤ g ⊓ 𝓟 (d.preimage ↑s)ᶜ

Tactic:
gcongr

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
φ : ι' → ι
⊢ UniformSpace.comap (fun g i' ↦ g (φ i')) (uniformSpace fun i' ↦ α (φ i')) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))

Tactic:
simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]

Goal state after:
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
this : x ∈ s
⊢ x ∈ t

Tactic:
specialize hst x; simp_all

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 β
f : α ≃ β
hf : IsUniformInducing ⇑f
⊢ UniformContinuous (⇑f ∘ f.invFun)

Tactic:
by simpa using uniformContinuous_id

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 β
F : ι → β → α
S T : Set β
H : UniformEquicontinuousOn F T
hST : S ⊆ T
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ 𝓤 β ⊓ 𝓟 (S ×ˢ S) ≤ 𝓤 β ⊓ 𝓟 (T ×ˢ T)

Tactic:
gcongr

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

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ UniformEquicontinuous (u ∘ Subtype.val)

Tactic:
by
  rw [← uniformEquicontinuousOn_univ] at hA ⊢
  exact hA.closure' (Pi.continuous_domRestrict _ |>.comp hu)

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

Goal state before:
pp: case mp.left
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * b ≤ a * y

Tactic:
gcongr

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

Goal state before:
pp: case mp.right
α : 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 ≤ a * c

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a + x) ∘ fun x ↦ -x) '' a_1 = (fun x ↦ a + x) '' (fun x ↦ -x) '' a_1
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
this : ∀ (a_1 : Set α), (fun x ↦ a + -x) '' a_1 = (fun x ↦ a + x) '' (fun x ↦ -x) '' a_1
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
⊢ IsQuotientMap ((fun x ↦ c • x) ∘ ⇑f)

Tactic:
by convert! hf.comp hc.isHomeomorph_smul.isQuotientMap; ext; simp

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ b * c < b * f x✝¹

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ b * f x✝¹ < b * c

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ c * b < f x✝¹ * b

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ f x✝¹ * b < c * b

Tactic:
gcongr

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
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (map Prod.fst l ×ˢ 𝓝 0) (𝓝 0)

Tactic:
· apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_fst hl

Goal state after:
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)
K_compact : IsCompact K
K_mem_l : K ∈ l
⊢ ∃ K ∈ l, IsCompact K

Tactic:
exact ⟨K, K_mem_l, K_compact⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun x ↦ b * x) ∘ fun x ↦ a * x) (cocompact M) (cocompact M)

Tactic:
convert! Filter.tendsto_id

Goal state after:
case e'_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ ((fun x ↦ b * x) ∘ fun x ↦ a * x) = id
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
y : G
hy : y ∈ closure[inst✝²] s
⊢ y ∈ s * s'

Tactic:
obtain ⟨_, ⟨b, hb, rfl⟩, hc⟩ :=
    mem_closure_iff_nhds.mp hy ((y * ·) '' s')
      (by simpa using (isOpenMap_mul_left y).image_mem_nhds hs'₀)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
y : G
hy : y ∈ closure[inst✝²] s
b : G
hb : b ∈ s'
hc : (fun x ↦ y * x) b ∈ s
⊢ y ∈ s * s'
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[>] a) = 𝓝[>] (c * a)

Tactic:
by
  convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [mul_comm]

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[<] a) = 𝓝[<] (c * a)

Tactic:
by
  convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp [mul_comm]

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

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ (∀ (x : G), 𝓝 x = comap (⇑f) (𝓝 (f x))) ↔ 𝓝 1 = comap (⇑f) (𝓝 1)

Tactic:
refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩

Goal state after:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x : G
⊢ 𝓝 x = comap (⇑f) (𝓝 (f x))
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: case refine_1
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
⊢ IsCompact ((y * x⁻¹) • K)

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
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
· exact hK.smul _

Goal state after:
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
⊢ (y * x⁻¹) • K ∈ 𝓝 y
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
⊢ f x✝¹ * g x✝¹ ≤ C * g x✝¹

Tactic:
gcongr

Goal state after:
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
⊢ f x✝¹ * g x✝¹ ≤ f x✝¹ * C

Tactic:
gcongr

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
⊢ ∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n

Tactic:
rcases (𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
  have :=
    ((hu.prod_nhds hu).tendsto_iff hu).mp
      (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
  simp only [and_self_iff, mem_prod, and_imp, Prod.forall, Prod.exists,
    forall_true_left] at this
  have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n := by
    intro n
    rcases this n with ⟨j, k, -, h⟩
    refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩
    rintro - ⟨a, ha, b, hb, rfl⟩
    exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
  obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
  exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩

Goal state after: