mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
by_cases hy : ClusterPt y l

Goal state after:
case pos
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (f '' univ)

Tactic:
exact isLindelof_univ.image hf

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
rcases Set.eq_empty_or_nonempty T with rfl | hT

Goal state after:
case refine_1.inl
X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen[inst✝] t
T_count : ∅.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ ∅ = ⋂ n, f n

case refine_1.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f n
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∀ (n : ℕ), IsOpen[inst✝] (f n)

Tactic:
simp_all

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ sᶜ ∩ tᶜ ∈ residual X

Tactic:
exact inter_mem hs ht

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 : Dense a✝ ∧ ∀ x ∈ s✝, Dense x
⊢ Dense (⋂₀ s✝)

Tactic:
exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
x✝ : X
⊢ x✝ ∈ ⋂ n, g n ∩ V n ↔ x✝ ∈ Subtype.val '' ⋂ n, f n

Tactic:
simp_all

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
f : ℕ → Set ↑s
V : ℕ → Set X
hV✝ : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
x✝ : X
hG : IsGδ (⋂ n, V n)
hd : Dense (⋂ n, V n)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
⊢ (∀ (i : ℕ), x✝ ∈ g i ∧ x✝ ∈ V i) ↔ ∃ (x : ∀ (i : ℕ), x✝ ∈ V i), ∀ (i : ℕ), ⟨x✝, ⋯⟩ ∈ f i
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)

Tactic:
apply dense_iInter_of_Gδ

Goal state after:
case ho
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)

case hd
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), Dense (bif s_1 then s else t)
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ f (a * b) = f 1

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ f (b * a) = f 1

Tactic:
simp_all

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

Goal state before:
pp: case refine_3
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ (↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ }, op ↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ }⁻¹) ∈ U ∧
    (map f) { val := a, inv := b, val_inv := ⋯, inv_val := ⋯ } = y

Tactic:
simp_all

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

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = ∅
⊢ f x = f y

Tactic:
simp_all

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

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = univ
⊢ f x = f y

Tactic:
simp_all

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id

Tactic:
Filter.ext_iff,

Goal state after:
X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ ∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s

Tactic:
exact fun z hz => hU (SetRel.prodMk_mem_comp hxy (ht <| mk_mem_prod hy hz)) 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 : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'

Tactic:
by
  simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
  rfl

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : SetRel α α), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i

Tactic:
exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : (Prod.map mk mk (y', z)).1 = (Prod.map mk mk (x, y)).2
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t

Tactic:
have : y' ⤳ y := (mk_eq_mk.1 hy).specializes

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : (Prod.map mk mk (y', z)).1 = (Prod.map mk mk (x, y)).2
this : y' ⤳ y
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ (if hc : UniformContinuous f then lift f ⋯ else fun x ↦ f ⋯.some) (mk a) = f a

Tactic:
dif_pos h,

Goal state after:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ lift f ⋯ (mk a) = f a
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔
    𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ∧ 𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ↔
    𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
α' : Type u_1
β' : Type u_2
inst✝¹ : UniformSpace α'
inst✝ : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : IsUniformInducing e₁
h₂ : IsUniformInducing e₂
⊢ comap (fun x ↦ ((e₁ x.1.1, e₂ x.1.2), e₁ x.2.1, e₂ x.2.2)) (𝓤 (α' × β')) = 𝓤 (α × β)

Tactic:
by simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ F.TotallyBounded

Tactic:
(hf.basis_uniformity (basis_sets _)).filter_totallyBounded_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ ∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id i) t ∈ F
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
simp only [mem_iUnion₂, mem_range]

Goal state after:
case refine_1
α : 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
⊢ ∀ (u : Set α), (∃ i, ∃ (_ : i ∈ s), ∃ y, ball i (t y) = u) → IsOpen[uniformSpace.toTopologicalSpace] u
Module: Mathlib.Topology.Coherent

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

Tactic:
simp_all

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, ball x U

Tactic:
simpa only [univ_subset_iff] using hs

Goal state after:
Module: Mathlib.Topology.Coherent

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

Tactic:
simp_all

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝¹ : Inv G₀
inst✝ : LinearOrder G₀
x y : G₀
h✝ : x ≤ y
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹

Tactic:
simp_all

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

Goal state before:
pp: case inr
G₀ : Type u_1
inst✝¹ : Inv G₀
inst✝ : LinearOrder G₀
x y : G₀
h✝ : y ≤ x
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹

Tactic:
simp_all

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 β
inst✝ : Finite ι
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
simp only [UniformEquicontinuous, eventually_all, @forall_comm _ ι]; rfl

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

Goal state before:
pp: case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
x : X
hx : x ∈ {x | (fun x ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x}
y : X
hy : y ∈ {x | (fun x ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x}
i : ι
⊢ (F i x, F i x₀) ∈ V

Tactic:
exact SetRel.symm V (hx i)

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₁ (u₁ ∩ u₂) v ⊆ t₁

pp: case refine_2
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₂ (u₁ ∩ u₂) w ⊆ t₂

Tactic:
· exact (image2_subset_right inter_subset_left).trans ht₁

Goal state after:
case refine_2
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₂ (u₁ ∩ u₂) w ⊆ t₂
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
          ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

Goal state after:
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 : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Goal state after:
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 : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
exact ⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

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

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun x ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
cases eq_or_lt_of_le hc
  · subst c
    simp [(nonempty_Icc.2 hab).image_const]
  exact image_mul_right_Icc' a b ‹0 < c›

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

Goal state before:
pp: case neg
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : ¬U ≠ ∅
⊢ IsOpen[inst✝⁵] U

Tactic:
simp_all

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

Goal state before:
pp: case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ

Goal state after:
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x ↦ 1 / f x
⊢ UniformContinuous fun x ↦ (f x)⁻¹

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
this : UniformContinuous fun x ↦ f x / (g x)⁻¹
⊢ UniformContinuous fun x ↦ f x * g x

Tactic:
simp_all

Goal state after: