mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClopen s ↔ frontier s = ∅

Tactic:
rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, sdiff_eq_empty]
  refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩
  exact ⟨(h.trans interior_subset).antisymm subset_closure,
    interior_subset.antisymm (subset_closure.trans h)⟩

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

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ ∀ (i : Bool), R1Space X

Tactic:
simp [*]

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

Goal state before:
pp: case tail
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ s j ∩ s k ⊆ s k ∩ ⋃ x ∈ p, s x

Tactic:
inter_comm

Goal state after:
case tail
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ s k ∩ s j ⊆ s k ∩ ⋃ x ∈ p, s x
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ tᶜ ∈ l

Tactic:
rw [← compl_subset_compl] at hsub

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s (succ k) ∩ s k).Nonempty

Tactic:
inter_comm

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ x ∈ s ∩ u'

Tactic:
inter_comm

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ y ∈ s ∩ v'

Tactic:
inter_comm

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
⊢ y ∈ v' ∩ s
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count

Goal state after:
case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → ↑c
f_surj : Function.Surjective f
⊢ ∃ f, s ⊆ ⋃ n, U (f n)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
have H1 := H (u ∩ s) (v ∩ s)

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst✝] (u ∩ s) →
    IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst✝¹] s = nhdsKer s

Tactic:
apply subset_antisymm

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst✝¹] s ⊆ nhdsKer s

case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ nhdsKer s ⊆ closure[inst✝¹] s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ u ∩ v ∩ s = ∅

Tactic:
inter_comm

Goal state after:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ∩ (u ∩ v) = ∅
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
constructor
  · intro h x
    apply h.1
    · exact subset_univ _
    exact isPreconnected_connectedComponent
  intro h; constructor
  intro s s_sub hs
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
  · exact subsingleton_empty
  · exact (h x).anti (hs.subset_connectedComponent x_in)

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
⊢ f x = f y

Tactic:
let F : S → T := hTm.restrict f S T
  suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
  rw [isDiscrete_iff_discreteTopology] at hT
  exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.mapsToRestrict _)

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

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t

pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X

Tactic:
· rw [mem_residual_iff]
    rintro ⟨S, hSo, hSd, Sct, Ss⟩
    refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩
    exact dense_sInter_of_isOpen hSo Sct hSd

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
⊢ Dense (⋃ i, interior (f i))

Tactic:
refine (hd.inter_of_Gδ hs (.iInter_of_isOpen fun i => (hgo i)) hgd).mono ?_

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
⊢ s ∩ ⋂ i, g i ⊆ ⋃ i, interior (f i)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
obtain ⟨V, hV, -, hV'⟩ := h x hx

Goal state after:
case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ (𝓟 s).TotallyBounded ↔ TotallyBounded s

Tactic:
simp only [Filter.TotallyBounded, mem_principal, SetRel.preimage_eq_biUnion, TotallyBounded]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded

Tactic:
rw [sSup_eq_iSup, totallyBounded_biSup hS]

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

Goal state before:
pp: case refine_2
α : 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
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Continuous[inst✝³.toTopologicalSpace, _] (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))

Tactic:
exact (continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactorization

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, IsOpen[inst✝¹] s_1

Tactic:
simp [*]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst✝¹] s
hs₂ : IsOpen[inst✝¹] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ s_1 ∈ {s, s'}, TendstoLocallyUniformlyOn F f p s_1

Tactic:
simp [*]

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 β
U : Set (α × α)
| 𝓤 β ⊓ 𝓟 (range (Prod.map Subtype.val Subtype.val))

Tactic:
← map_comap

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
U : Set (α × α)
| map (Prod.map Subtype.val Subtype.val) (Filter.comap (Prod.map Subtype.val Subtype.val) (𝓤 β))
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x✝ : Set γ
⊢ x✝ ∈ {s | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} ↔ x✝ ∈ map (uncurry m) (f ×ˢ g)

Tactic:
by
    simp only [mem_map, mem_prod_iff, image2_subset_iff, prod_subset_iff]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map (fun p ↦ m p.1 p.2) (map (Prod.mk a) g) = map (m a) g

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun p ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map (fun p ↦ m p.1 p.2) (map (fun a ↦ (a, b)) f) = map (fun x ↦ m x b) f

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun a ↦ (a, b)) f = map (fun x ↦ m x b) f
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map (fun p ↦ m p.1 p.2) (f ×ˢ g)) = map (fun p ↦ n (m p.1 p.2)) (f ×ˢ g)

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun p ↦ m p.1 p.2) (f ×ˢ g) = map (fun p ↦ n (m p.1 p.2)) (f ×ˢ g)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) =
    map (fun p ↦ m' p.1 (n' p.2.1 p.2.2)) (map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h))

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) =
    map ((fun p ↦ m' p.1 (n' p.2.1 p.2.2)) ∘ ⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f

Tactic:
← uniformContinuousOn_univ,

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuousOn f univ
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
ext x
  constructor
  · rintro ⟨y, ⟨hby, hyc⟩, rfl⟩
    dsimp
    constructor <;> gcongr
  · rintro ⟨habx, hxac⟩
    obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
    refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxac

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure 1 = 1

Tactic:
pure_one

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ 1 = 1
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
x : ↑s
hf : ContinuousOn f s
⊢ (mkD (s.domRestrict f) g) x = f ↑x

Tactic:
mkD_of_continuousOn hf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
x : ↑s
hf : ContinuousOn f s
⊢ { toFun := s.domRestrict f, continuous_toFun := ⋯ } x = f ↑x
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
left; rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₁ * r₂ = 1

Tactic:
symm
    simpa using h₁.mul h₂

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:
← sInf_range

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)

Tactic:
by simpa only [one_mul] using! hs

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

Goal state before:
pp: M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
← sInf_range

Goal state after:
M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
← sInf_range

Goal state after:
G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : DiscreteTopology ↥𝒢
⊢ DiscreteTopology ↥(h • 𝒢)

Tactic:
by
  simp only [← SetLike.coe_sort_coe, ← isDiscrete_iff_discreteTopology] at *
  refine IsDiscrete.image_of_isOpenMap ‹_› ?_ fun x y ↦ by simp
  apply IsOpenMap.of_inverse (f' := fun x ↦ h⁻¹ • x) (continuous_const_smul _) <;>
  · intro x
    simp

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

Goal state before:
pp: case right
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x k : A
hk : φ k = 1
hx : x ∈ (fun h ↦ (fun x ↦ x * k) ⁻¹' U) hk
⊢ φ (x * k) = φ x

Tactic:
rw [map_mul, hk, mul_one]

Goal state after: