mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case fst
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).1 = (p, q).1

pp: case snd
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
· exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget GrpCat.{u}) G H) (p, q)

Goal state after:
case snd
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).2 = (p, q).2
Module: Mathlib.Algebra.Category.ModuleCat.Injective

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
ext x; simpa using h x

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ (match n with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      n =
    a

Tactic:
cases n

Goal state after:
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ (match ofNat a✝ with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      ofNat a✝ =
    a

case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (match -[a✝+1] with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      -[a✝+1] =
    a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)

Tactic:
by
  simpa only [nsmul_eq_mul] using h.nsmul n

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
by
  rw [← add_assoc, h, h.nat_even_mul_periodic]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • (c + c))

Tactic:
← two_nsmul

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (↑n) (↑n + 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

Goal state after:
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (b + a) = count (fun k ↦ p (k + b)) a + count p b

Tactic:
count_add,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p b + count (fun k ↦ p (b + k)) a = count (fun k ↦ p (k + b)) a + count p b
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : count p a < count p (a + (k + 1))
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x

Tactic:
count_add,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : count p a < count p a + count (fun k ↦ p (a + k)) (k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

Tactic:
simpa [frequently_atTop] using high_scores hu

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : 2 * φ a = φ a
ha' : ¬a = 0
h : 2 * a = b
⊢ False

Tactic:
mul_eq_right (totient_eq_zero.not.mpr ha')

Goal state after:
case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : 2 = 1
ha' : ¬a = 0
h : 2 * a = b
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [Nat.pow_div h hp.pos]

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
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 : α
⊢ toIocMod hp a a = a + p

Tactic:
toIocMod_eq_iff hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p ∈ Set.Ioc a (a + p) ∧ ∃ z, a = a + p + z • p
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 : α
⊢ toIocMod hp a (a + p) = a + p

Tactic:
toIocMod_eq_iff hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p ∈ Set.Ioc a (a + p) ∧ ∃ z, a + p = a + p + z • p
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_

Goal state after:
case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ DirectedOn (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) f.sets

case refine_2
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s

Tactic:
by
  simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]

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) = p - toIcoMod hp (-a) b

Tactic:
simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]
  abel

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 c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
← two_nsmul

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) = 2 • p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
Module: Mathlib.Topology.Order

Goal state before:
pp: case mpr
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := ⋯
⊢ (∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t

Tactic:
rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩

Goal state after:
case mpr
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen[T] v
amem : f a ∈ v
⊢ ∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
Module: Mathlib.Topology.Order

Goal state before:
pp: case mpr
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := ⋯
⊢ (∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t

Tactic:
· rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
    exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩

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
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
rw [isQuotientMap_iff]
  refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩
  exact ⟨fun h => surj.image_preimage s ▸ open_map _ h, fun h => h.preimage cont⟩

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 : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∃ᶠ (y : Y) in 𝓝 y₀, ∃ x ∈ f ⁻¹' {y}, p x
⊢ ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in 𝓝 x₀, p x

Tactic:
contrapose! H
  exact hf.eventually_nhds_fiber y₀ H

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rw [Tendsto, ← map_map, hf.map_nhds_eq]; rfl

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 : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
by
  rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]

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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
x✝ : X × Y
a : X
b : Y
⊢ pure a ×ˢ pure b = pure (a, b)

Tactic:
prod_pure_pure

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
x✝ : X × Y
a : X
b : Y
⊢ pure (a, b) = pure (a, b)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Tactic:
by
  rw [← Iio_union_Ioi, nhdsWithin_union]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Tactic:
rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
simp_rw [nhdsWithin_eq, tendsto_iInf, mem_ofPred_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)

Tactic:
rintro ⟨a, b⟩

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)

Tactic:
by
  refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩
  · rw [← image_domRestrict]
    exact h _ (ht.preimage continuous_subtype_val)
  · rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] {x}

Tactic:
← univ_pi_singleton

Goal state after:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] (univ.pi fun i ↦ {x i})
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ s ⊆ ⋃ i, (interior ∘ ⇑K) i

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) (interior ∘ ⇑K)

Tactic:
· intro x _
    rcases K.exists_mem x with ⟨k, hk⟩
    exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) (interior ∘ ⇑K)
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
D E : Set ↑A
⊢ D ⊆ A ↓∩ Subtype.val '' E ↔ D ⊆ E

Tactic:
rw [preimage_image_eq _ Subtype.val_injective]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Tactic:
← continuousWithinAt_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousWithinAt (update f x y) univ x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s

Tactic:
map_mk_nhds

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ 𝓝 (mk x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact univ

Tactic:
← pi_univ univ

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (univ.pi fun i ↦ univ)
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 X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
⊢ IsDiscrete (f '' s)

Tactic:
refine .of_nhdsWithin ?_
  rintro _ ⟨x, hx, rfl⟩
  rw [← map_pure, ← hs.nhdsWithin x hx, nhdsWithin, nhdsWithin, map_inf hf', map_principal]
  grw [hf.nhds_le x]

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
⊢ V'ᶜ = U

Tactic:
refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)

Goal state after:
case refine_1
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
⊢ Sᶜ ⊆ V'ᶜ

case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
⊢ V'ᶜᶜ.Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : ↑(irreducibleComponents Y)
⊢ (↑W ∩ range f).Nonempty

Tactic:
simp [hf₄.range_eq, W.2.1.1]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x

Tactic:
refine nhdsWithin_mono x hu ?_

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
⊢ f x ≠ g x

Tactic:
by_contra H

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_connected_basis]
  exact fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
by
  refine ⟨fun hs => ?_, ?_⟩
  · obtain rfl | h := s.eq_empty_or_nonempty
    · exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩
    · obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
      exact ⟨a, t, ht.isPreconnected, rfl⟩
  · rintro ⟨a, t, ht, rfl⟩
    exact ht.image _ continuous_sigmaMk.continuousOn

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

Goal state before:
pp: case refine_1.inr.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : (inr '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1

Tactic:
exact Or.inr ⟨t, ht.isPreconnected, rfl⟩

Goal state after:
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_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (univ \ s i)

Tactic:
← h_Union,

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] ((⋃ i, s i) \ s i)
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)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (univ \ s i)

Tactic:
← h_Union,

Goal state after:
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] ((⋃ i, s i) \ s i)