mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ Subsingleton ι

Tactic:
rw [← not_nontrivial_iff_subsingleton]
  by_contra ⟨i, j, h_ne⟩
  replace h_ne : s i ∩ s j = ∅ := by
    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne
  rcases isClopen_iff.mp (h_clopen i) with hi | hi
  · exact (h_nonempty i).ne_empty hi
  · rw [hi, univ_inter] at h_ne
    exact (h_nonempty j).ne_empty h_ne

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
⊢ P x y

Tactic:
have A : IsClosed u := by
    apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
    rcases hz _ (h z) with ⟨t, ht, h't⟩
    exact h'.trans x t z h't ht.2

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
⊢ P x y
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:
by
  apply subset_antisymm
  · rw [nhdsKer, ← hs.lift'_closure_nhdsSet]
    simp +contextual [Filter.lift', Filter.lift, closure_mono, subset_of_mem_nhdsSet]
  · intro y hy
    by_contra! hy'
    rw [← _root_.disjoint_nhdsSet_nhds, Filter.disjoint_iff] at hy'
    obtain ⟨t, hts, t', ht'y, H⟩ := hy'
    exact Set.disjoint_iff.mp H ⟨hy t hts, mem_of_mem_nhds ht'y⟩

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

Goal state before:
pp: case mpr
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
⊢ (∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i) → IsLindelof U ∧ IsOpen[inst✝] U

Tactic:
· rintro ⟨s, hs, rfl⟩
    constructor
    · exact hs.isLindelof_biUnion fun i _ => hb' i
    · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst✝¹] (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)

Tactic:
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst✝¹] (f '' s i) ⊆ T
⊢ closure[inst✝¹] (f '' s i) ∈ 𝓝 (f x)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
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
hne : T.Nonempty
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
by
  rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
  · exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩
  · exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hT hc hTm hx' hx⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ IsMeagre s

Tactic:
by
  rw [isMeagre_iff_countable_union_isNowhereDense]
  exact ⟨{s}, by simpa, by simp, by simp⟩

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

Goal state before:
pp: 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
ι' : Type u_8
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpaceProd] (Equiv.sumArrowEquivProdArrow ι ι' X).toFun

Tactic:
dsimp [Equiv.sumArrowEquivProdArrow]
    fun_prop

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

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

Tactic:
rintro x hx
  by_contra! h
  simpa [U.rfl] using h _ <| hN.2 (y := insert x N) ⟨by simp [insert_subset_iff, hx, hN.1.1],
    hN.1.2.insert fun y hy hxy ↦ (h y hy hxy).elim⟩ (subset_insert _ _) (mem_insert _ _)

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (fun x ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l

Tactic:
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f

Tactic:
by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h

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

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

Tactic:
rintro ⟨V, V_in, _, V_sub⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : f ×ˢ f ≤ 𝓤 α
⊢ ∃ x, f = pure x

Tactic:
simp only [DiscreteUniformity.eq_principal_setRelId, le_principal_iff, mem_prod_iff] at f_le

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id
⊢ ∃ x, f = pure x
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : (𝓤 α).IsCountablyGenerated
inst✝¹ : UniformSpace β
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (𝓤 (α × β)).IsCountablyGenerated

Tactic:
by
  rw [uniformity_prod]
  infer_instance

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
⊢ (⨆ x, 𝓟 (s x)).TotallyBounded ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded

Tactic:
Filter.totallyBounded_iSup

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
⊢ Tendsto f p' (𝓝 ℓ)

Tactic:
by
  rw [tendsto_nhds_left]
  intro s hs
  rw [mem_map, Set.preimage, ← eventually_iff]
  obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
  have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
  have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
  have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry
  obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists
  filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩

Goal state after:
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 ∧ mulSupport f ⊆ K) ↔ HasCompactMulSupport f

Tactic:
hasCompactMulSupport_def,

Goal state after:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ mulSupport f ⊆ K) ↔ IsCompact (closure[inst✝²] (mulSupport f))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One β
inst✝ : One γ
g : β → γ
f : α → β
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f

Tactic:
hasCompactMulSupport_def,

Goal state after:
α : Type u_2
β : Type u_4
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One β
inst✝ : One γ
g : β → γ
f : α → β
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ IsCompact (closure[inst✝²] (mulSupport (g ∘ f))) ↔ IsCompact (closure[inst✝²] (mulSupport f))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)

Tactic:
hasCompactMulSupport_def,

Goal state after:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure[inst✝¹] (mulSupport (f ∘ g)))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f

Tactic:
compl_subset_comm

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t : Set β
⊢ ∀ ⦃t_1 : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t_1, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t_1, (f p x, f q x) ∈ u

Tactic:
t'

Goal state after:
case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) →
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: case mpr
ι : 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 : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rcases H U hU with ⟨V, hV, hVU⟩

Goal state after:
case mpr
ι : 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 : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝[S] x₀
hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
by
  simp only [iInf_uniformity]
  exact
    hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
      (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
      (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * c * y ∈ Icc a b * Icc c d

Tactic:
refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * y ≤ b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iio]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iio]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
    exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

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

Goal state before:
pp: M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n x✝ : ℕ
ihn : (a ^ x✝) ⤳ (b ^ x✝)
⊢ (a ^ x✝.succ) ⤳ (b ^ x✝.succ)

Tactic:
by
    simpa only [pow_succ] using ihn.mul h

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)

Tactic:
rw [mul_singleton]
  exact smul_mem_nhds_smul (op a) h

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ⇑f
⊢ IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker

Tactic:
apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (1 * 1⁻¹))

Tactic:
apply Continuous.tendsto (by fun_prop)

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

Goal state before:
pp: α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] {p | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}

Tactic:
refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_) <;>
    fun_prop

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

Tactic:
simpa only [Function.update_self] using! h i (mem_univ i)

Goal state after:
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}
H : t.Countable
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]

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}
H : t.Countable
this : {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x}
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
⊢ ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)

Tactic:
refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Goal state after:
R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia, 0 < ia ∧ ∀ x ∈ {x | norm x < ia}, f x ∈ {x | norm x < ε}
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
· exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = Preorder.topology αᵒᵈ

Tactic:
simp_rw [Preorder.topology, or_comm]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t.OrdConnected
⊢ (range Subtype.val).OrdConnected

Tactic:
← @Subtype.range_val _ t

Goal state after:
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : (range Subtype.val).OrdConnected
⊢ (range Subtype.val).OrdConnected
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ 1 • 1 = (fun x ↦ LinearMap.id ↑n • x) (↑n)⁻¹

Tactic:
simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) ↑(addOrderOf a) = 0

Tactic:
rw [h, Nat.cast_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (Submodule.liftQSpanSingleton (↑(addOrderOf a))
            (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) ⋯ ∘ₗ
          ↑(intSpanEquivQuotAddOrderOf a)).toAddMonoidHom
      ⟨a, ⋯⟩ =
    0
⊢ a = 0

Tactic:
LinearMap.toAddMonoidHom_coe,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (Submodule.liftQSpanSingleton (↑(addOrderOf a))
          (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) ⋯ ∘ₗ
        ↑(intSpanEquivQuotAddOrderOf a))
      ⟨a, ⋯⟩ =
    0
⊢ a = 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : 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'
⊢ (Disjoint on fun x ↦ Ioc (z x) x) x x'

Tactic:
rcases hxx'.lt_or_gt with (h' | h')
    · refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
    · 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.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
· apply continuousWithinAt_toIcoMod_Ici

Goal state after: