mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Set α
⊢ ∀ (v : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
v

Goal state after:
α : 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 α
⊢ IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst✝] s → IsLindelof s
⊢ HereditarilyLindelofSpace X

Tactic:
refine ⟨fun s _ ↦ isLindelof_of_countable_subcover fun U U_open hU ↦ ?_⟩
  obtain ⟨t, t_count, ht⟩ := H (⋃ i, U i) (isOpen_iUnion U_open)
    |>.elim_countable_subcover U U_open subset_rfl
  exact ⟨t, t_count, hU.trans ht⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure[inst✝] (e '' {x | p x})
hx : x ∈ closure[inst✝] (range fun x ↦ e ↑x)
⊢ ⟨x, hx✝⟩ ∈ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) ↔ ⟨x, hx✝⟩ ∈ univ

Tactic:
simpa [closure_subtype, ← range_comp, (· ∘ ·)]

Goal state after:
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
U : SetRel X X
s N : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
hN : Maximal (fun N ↦ N ⊆ s ∧ U.IsSeparated N) N
⊢ U.IsCover s N

Tactic:
rintro x hx

Goal state after:
X : Type u_1
U : SetRel X X
s N : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
hN : Maximal (fun N ↦ N ⊆ s ∧ U.IsSeparated N) N
x : X
hx : x ∈ s
⊢ ∃ y, y ∈ N ∧ (x, y) ∈ U
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Fin.appendEquiv m n = (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Tactic:
apply Equiv.symm_bijective.injective

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ (Fin.appendEquiv m n).symm = (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝² : DiscreteUniformity X
Y : Type u_2
inst✝¹ : UniformSpace Y
inst✝ : DiscreteUniformity Y
⊢ DiscreteUniformity (X × Y)

Tactic:
simp [discreteUniformity_iff_eq_principal_setRelId, uniformity_prod_eq_comap_prod,
    eq_principal_setRelId, SetRel.id, Set.prod_eq, Prod.ext_iff, Set.ofPred_and]

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 α
F' : ι → α → β
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F x.1 x.2) ∈ id i
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F' x.1 x.2) ∈ id i

Tactic:
exact fun i hi => (hf i hi).congr (hff'.mono fun x hx =>
    (Inseparable.rfl.prod hx).mem_open_iff hi.2)

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ 𝓝 x

Tactic:
by
  simp [completeSpace_iff_isComplete_univ, isComplete_iff_ultrafilter]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst✝.toTopologicalSpace] (UniformSpace.ball (e a) U)
⊢ closure[inst✝.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Tactic:
refine mem_of_superset (ho.mem_nhds <| UniformSpace.mem_ball_symmetry.2 ha) fun y hy => ?_

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst✝.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure[inst✝.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
Filter.HasBasis.totallyBounded_iff H

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ ∀ (i : ℕ), p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
⊢ ∀ x ∈ ⋃ x ∈ s, t x, (f x, g x) ∈ r

Tactic:
rintro x hx

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : x ∈ ⋃ x ∈ s, t x
⊢ (f x, g x) ∈ r
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N

Tactic:
exact setSeq_mono hf U_mem hm hp.1

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y

Tactic:
rcases lebesgue_number_lemma (U := fun x => interior (U x)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
V : Set (α × α)
V_uni : V ∈ 𝓤 α
hV : ∀ x ∈ K, ∃ i, ball x V ⊆ interior (U i)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s

Tactic:
have := le_max_left m n
        exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm

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
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
have de : IsDenseEmbedding e := he.isDenseEmbedding hd
  have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
  have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
    isUniformEmbedding_subtypeEmb _ he de
  have : b ∈ closure (e '' { x | p x }) :=
    (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
  let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
  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
  refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
  rw [Subtype.range_coe_subtype]
  exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩

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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U

Tactic:
by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ SecondCountableTopology α

Tactic:
choose ht_mem hto hts using hto

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ SecondCountableTopology α
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
x : α
⊢ ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) x = (SeparationQuotient.mk ∘ f) x

Tactic:
simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)

Goal state after:
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous[inst✝, _] f
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)
⊢ IsOpen[inst✝] u

Tactic:
simp only [continuousOn_iff_continuous_domRestrict, continuous_Prop] at *
    exact h _ hu

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ i, uniformSpace α γ

Tactic:
by
  -- This follows directly from the fact that the upper adjoint in a Galois connection maps
  -- infimas to infimas.
  ext : 1
  change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]
  rw [iInf_uniformity, iInf_uniformity]
  exact (UniformFun.gc α γ).u_iInf

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 : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous Subtype.val

Tactic:
rw [← comp_rangeSplitting F]; exact h.comp _

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 : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn Subtype.val S

Tactic:
rw [← comp_rangeSplitting F]; exact h.comp _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i ↦ p i.2) fun i ↦ UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Tactic:
have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
  have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦ by
    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
  refine (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩
  rcases hex s hs with ⟨i, hi⟩
  exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousOn F S ↔ EquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S

Tactic:
congrm ∀ x ∈ S, ?_

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt ((fun x ↦ u ∘ x) ∘ F) S x
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 : α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ a * b * y ∈ a • Icc b c

Tactic:
refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ b * y ≤ c
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a

Tactic:
by
  simp only [isUnit_iff, Group.isUnit, and_true]

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ x + b) '' Ioc (a * c) (a * d) = Ioc (a * c + b) (a * d + b)

Tactic:
image_add_const_Ioc

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ Ioc (a * c + b) (a * d + b) = Ioc (a * c + b) (a * d + b)
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:
convert! hf.comp hc.isHomeomorph_smul.isQuotientMap; ext; simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
by
  rw [← sInf_range]
  exact isUniformGroup_sInf (Set.forall_mem_range.mpr 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
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y})) inf_le_right 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
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (mk ⁻¹' mk '' s) ↔ Dense (s * ↑N)

Tactic:
preimage_image_mk_eq_mul

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (s * ↑N) ↔ Dense (s * ↑N)
Module: Mathlib.Topology.Algebra.Group.Quotient

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

Tactic:
preimage_image_mk_eq_mul

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

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

Tactic:
refine eq_of_forall_le_iff fun 𝓕 ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

Tactic:
refine eq_of_forall_le_iff fun 𝓕 ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
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
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (⇑f) (𝓝 (f x))

Tactic:
← nhds_translation_mul_inv (f 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
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (⇑f) (comap (fun x_1 ↦ x_1 * (f x)⁻¹) (𝓝 1))
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
by rwa [map_one] at this

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

Goal state before:
pp: α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
this :
  map (fun t ↦ t.2 - t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) ×ˢ
      map (fun t ↦ t.2 - t.1) (comap (fun p ↦ (f p.1, f p.2)) (𝓝 (y₀, y₀))) ≤
    𝓝 0 ×ˢ 𝓝 0
⊢ Tendsto (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0)

Tactic:
prod_map_map_eq

Goal state after:
α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
this :
  map (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
      (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀)) ×ˢ comap (fun p ↦ (f p.1, f p.2)) (𝓝 (y₀, y₀))) ≤
    𝓝 0 ×ˢ 𝓝 0
⊢ Tendsto (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0)