mathlib-initiative/mathlib-tactics huggingface dataset:
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)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
x : Y
⊢ (∀ (i : ℕ), x ∈ f i) ↔ ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst✝²] s

Tactic:
refine ⟨fun h i => by grind, fun h i => ?_⟩

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)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
x : Y
h : ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst✝²] s
i : ℕ
⊢ x ∈ f i
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h ⁻¹' s) ↔ IsCompact s

Tactic:
rw [← image_symm]; exact h.symm.isCompact_image

Goal state after:
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
  ext x i <;> simp

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case pos
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'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : DecidablePred p
j : ι
h✝ : p j
⊢ Continuous[instTopologicalSpaceProd, inst✝¹ j] fun a ↦ a.1 ⟨j, h✝⟩

pp: case neg
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'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : DecidablePred p
j : ι
h✝ : ¬p j
⊢ Continuous[instTopologicalSpaceProd, inst✝¹ j] fun a ↦ a.2 ⟨j, h✝⟩

Tactic:
exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
connectedSpace_iff_univ,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ IsConnected univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

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

Tactic:
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

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

Goal state before:
pp: case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
⊢ ∀ l ≥ N + k, (u a, u l) ∈ V

Tactic:
b

Goal state after:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
⊢ b ≥ N + k → (u a, u b) ∈ V
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s

Tactic:
exact fun _ x s hs ↦ refl_mem_uniformity hs

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

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
⊢ (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t

Tactic:
by
  ext
  simp only [mem_entourageProd, SetRel.mem_image, Set.mem_prod, Prod.exists]
  grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
⊢ UniformContinuous (lift' f)

Tactic:
by_cases hf : UniformContinuous f
  · rwa [lift', dif_pos hf, uniformContinuous_lift]
  · rw [lift', dif_neg hf]
    exact uniformContinuous_of_const fun a _ => rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
⊢ ∀ (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
⊢ a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

Tactic:
by
  simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]

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

Goal state before:
pp: case refine_2
α : 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
x : α
⊢ ∀ (u : Set α),
    x ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), x ∈ v ∧ v ⊆ u

Tactic:
V

Goal state after:
case refine_2
α : 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
x : α
V : Set α
⊢ x ∈ V → IsOpen[uniformSpace.toTopologicalSpace] V → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), x ∈ v ∧ v ⊆ V
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ SetRel.symmetrize {x | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r}
h₁ : b₁ ∉ s
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

Tactic:
by_cases h₂ : b₂ ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ SetRel.symmetrize {x | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r}
h₁ : b₁ ∉ s
h₂ : b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}

case neg
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ SetRel.symmetrize {x | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r}
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
by
  rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩
  have : UniformContinuousOn ↿f (K ×ˢ univ) :=
    IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
      (h.mono <| prod_mono hKU Subset.rfl)
  exact this.tendstoUniformly hxK

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

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

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖

Tactic:
← UniformSpace.ext hf,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a ↦ (Multiset.map (fun i ↦ f i a) s).prod) t

Tactic:
by
  rcases s with ⟨l⟩
  simpa using continuousOn_list_prod l

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
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T1Space G

Tactic:
refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
⊢ False
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x

Tactic:
← @nhds_translation_mul_inv G t' _ _ x,

Goal state after:
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
← one_mul 1

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (1 * 1))
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_
  · exact ⟨univ, by simp⟩
  · rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
  · rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')
  · intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

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

Tactic:
refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
by
  if hb : BddAbove (range f) then
    exact hf.ciSup_comp_tendsto_atTop hb hg
  else
    rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
    rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
  simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
⊢ ∀ (b ε : G), ε > 1 → ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
b

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b : G
⊢ ∀ ε > 1, ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
h𝓤GN.cauchySeq_iff

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : ∀ (i : ℕ), True → ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → (x m, x n) ∈ {x | x.2 / x.1 ∈ mk '' u i}
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
⊢ ∀ ⦃y_1 : α⦄, y_1 ∈ t → a ≠ y_1 → Disjoint (Ioo a (y a)) (Ioo y_1 (y y_1))

Tactic:
b

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
⊢ b ∈ t → a ≠ b → Disjoint (Ioo a (y a)) (Ioo b (y b))
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
by
  simp only [div_eq_mul_inv]
  exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

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 α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
⊢ LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

Tactic:
rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

case inr
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (s ∩ e.source) = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
e.leftInvOn.image_inter',

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e.symm ⁻¹' s ∩ ↑e '' e.source = e.target ∩ ↑e.symm ⁻¹' s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
⊢ induced f t = Preorder.topology α

Tactic:
refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y

case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
⊢ (Disjoint on fun x ↦ Ioc (z x) x) x x'

Tactic:
· refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
      refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : MonCat
⊢ (MonoidalCategoryStruct.whiskerRight (↾fun x ↦ 1) ↑A ≫ ↾fun p ↦ p.1 * p.2) =
    (MonoidalCategoryStruct.leftUnitor ↑A).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : MonCat
⊢ (MonoidalCategoryStruct.whiskerLeft (↑A) (↾fun x ↦ 1) ≫ ↾fun p ↦ p.1 * p.2) =
    (MonoidalCategoryStruct.rightUnitor ↑A).hom

Tactic:
by cat_disch

Goal state after: