mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ ∀ (x_1 : X) (h : (ConcreteCategory.hom c.inl) x_1 = (ConcreteCategory.hom c.inr) x),
    (ConcreteCategory.hom f)
        ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
      (ConcreteCategory.hom g) x

Tactic:
intro y e

Goal state after:
case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
nth_rw 3 [this]

Goal state after:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p - b = -(b - toIcoDiv hp a b • p)

Tactic:
neg_sub

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p - b = toIcoDiv hp a b • p - b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = -(b - toIocDiv hp a b • p)

Tactic:
neg_sub

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = toIocDiv hp a b • p - b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1

Tactic:
by
  rw [add_comm, toIocDiv_add_right]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ c - b = (toIocDiv hp a c - toIocDiv hp a b) • p

Tactic:
conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
    rw [h, sub_smul]
    abel

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
    at this

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
by
  rwa [ClusterPt, inf_eq_right.mpr H]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a

Tactic:
by
  rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False

Tactic:
accPt_principal_iff_clusterPt

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
⊢ False
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Icc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
    iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst✝] (s ∪ t)
⊢ IsOpen[inst✝] s

Tactic:
by
  obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
  suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu
  rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen s

Tactic:
simp +instances only [sSup_eq_iSup, isOpen_iSup_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})

Tactic:
nhdsSet_iUnion,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (⋃ i ∈ s, f ⁻¹' {i})

Tactic:
nhdsSet_iUnion,

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (⨆ i ∈ s, 𝓝ˢ {i}) ≤ ⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i})
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ IsOpenEmbedding f

Tactic:
by
  simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
    and_true]
  exact fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst✝] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
nhdsWithin_restrict t h₀ h₁,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst✝] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u] a
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : { x // x ∈ s }
⊢ 𝓝 x = comap Subtype.val (𝓝[s] ↑x)

Tactic:
nhds_subtype,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : { x // x ∈ s }
⊢ comap Subtype.val (𝓝 ↑x) = comap Subtype.val (𝓝[s] ↑x)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝[s i] x i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))

Tactic:
by
  simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
    comap_principal]
  rw [iInf_split _ fun i => i ∈ I, inf_right_comm]
  simp only [iInf_inf_eq]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝 a ⊓ 𝓟 u ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
nhds_subtype,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ comap Subtype.val (𝓝 ↑a) ⊓ 𝓟 u ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ (∀ (b : Bool), IsOpen[inst✝] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})

Tactic:
Bool.forall_bool' b,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)

Tactic:
cases b

Goal state after:
case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif false then s else t)

case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif true then s else t)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ False

Tactic:
have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
    refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
    rcases hV i j with ⟨k, hki, hkj⟩
    refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
      tauto

Goal state after:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this : (⋂ i, V i ∩ Wᶜ).Nonempty
⊢ False
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ (mk '' mk ⁻¹' t))

Tactic:
comap_mk_nhdsSet_image

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
| 𝓝ˢ (mk ⁻¹' t)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (𝓝[s] f x) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
← (hf.continuousWithinAt hx
    |>.tendsto_nhdsWithin fun _ ↦ by exact id).le_comap,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ 𝓝[f ⁻¹' s] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ (insert z ∅).Finite
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] (const X y '' s)

Tactic:
by simp_rw [const, h2s.image_const, isClosed_singleton]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
l : Filter Y
inst✝ : l.NeBot
c d : X
⊢ Tendsto (fun x ↦ c) l (𝓝 d) ↔ c = d

Tactic:
simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : s ∈ codiscreteWithin K
⊢ (K \ s).Finite

Tactic:
rw [mem_codiscreteWithin_accPt] at hs
  contrapose! hs
  exact Set.Infinite.exists_accPt_of_subset_isCompact hs hK (sep_subset _ _)

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous[inst✝, _] U.boolIndicator ↔ IsClopen U

Tactic:
continuous_bool_rng true,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
U : Set X
⊢ IsClopen (U.boolIndicator ⁻¹' {true}) ↔ IsClopen U
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
⊢ IsOpen[inst✝¹] (connectedComponentIn F x)

Tactic:
rw [isOpen_iff_mem_nhds]
  intro y hy
  rw [connectedComponentIn_eq hy]
  exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ n, s n)

Tactic:
by
  rw [← biUnion_univ]
  exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
    simpa [mem_univ] using K i j

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)

Tactic:
by
  refine ⟨fun S hSc hS => ?_⟩
  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
  exact (countable_bInter_mem hSc).2 hS

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
b : Bool
⊢ IsLindelof (bif b then s else t)

Tactic:
cases b

Goal state after:
case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif false then s else t)

case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif true then s else t)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)

Tactic:
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
  rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
  refine mem_of_superset (hUo.mem_nhds haU) ?_
  calc
    U ⊆ closure (i '' i ⁻¹' U) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_mono sub)

Goal state after:
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:
exact Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
by simp_rw [subset_def, mem_ofPred, forall_and, and_assoc]

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

Goal state before:
pp: case insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝ : Set X
s✝ : Set (Set X)
ha : a✝ ∉ s✝
hsf : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → (∀ t ∈ s✝, Dense t) → Dense (⋂₀ s✝)
ho : ∀ t ∈ insert a✝ s✝, IsOpen[inst✝] t
hd : ∀ t ∈ insert a✝ s✝, Dense t
⊢ Dense (⋂₀ insert a✝ s✝)

Tactic:
simp only [sInter_insert, forall_mem_insert] at hd ⊢

Goal state after:
case insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝ : Set X
s✝ : Set (Set X)
ha : a✝ ∉ s✝
hsf : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → (∀ t ∈ s✝, Dense t) → Dense (⋂₀ s✝)
ho : ∀ t ∈ insert a✝ s✝, IsOpen[inst✝] t
hd : Dense a✝ ∧ ∀ x ∈ s✝, Dense x
⊢ Dense (a✝ ∩ ⋂₀ s✝)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ ∃ x ∈ U i, x ∈ U j

Tactic:
exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩

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

Goal state before:
pp: α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ g ×ˢ f ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f

Tactic:
← SetRel.inv,

Goal state after:
α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ g ×ˢ f ↔ R.inv ∈ g ×ˢ f
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift f

Tactic:
by
      rw [lift_lift'_assoc]
      · exact monotone_id.relComp monotone_id
      · exact h

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
conv =>

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

Goal state before:
pp: case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
rintro ⟨V, V_in, V_sub⟩

Goal state after:
case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ 𝓝 x✝ ⊓ 𝓝 x✝ = comap (Prod.mk x✝) (𝓤 α ⊓ 𝓤 α)

Tactic:
@nhds_eq_comap_uniformity _ u₁,

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ comap (Prod.mk x✝) (𝓤 α) ⊓ 𝓝 x✝ = comap (Prod.mk x✝) (𝓤 α ⊓ 𝓤 α)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 SetRel.id

Tactic:
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))
  calc
    comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
    _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
    _ ≤ 𝓟 SetRel.id := principal_mono.2 ?_
  rintro ⟨x, y⟩; simpa [not_imp_not] using @hf x y

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

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

Tactic:
refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi

Goal state after:
case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
x✝ : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p s
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ TendstoLocallyUniformlyOn (fun x ↦ g ∘ F x) (g ∘ f) p s

Tactic:
by
  rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
  refine fun x hx ↦ Tendsto.comp hg (tendsto_inf.mpr ⟨hf x hx, tendsto_principal.mpr ?_⟩)
  filter_upwards [hFs.prod_mk eventually_mem_nhdsWithin] with y hy using ⟨hfs hy.2, hy.1 hy.2⟩

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) ((fun i ↦ uniformSpace α (δ i)) i)) =
    uniformSpace α ((i : ι) → δ i)

Tactic:
rw [← UniformSpace.comap_comap, UniformFun.comap_eq]

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) ((fun i ↦ uniformSpace α (δ i)) i) =
    UniformSpace.comap (fun x ↦ Function.eval i ∘ x) (uniformSpace α (δ i))