mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ s.π.app zero ≫ f j = s.π.app one

Tactic:
by
  rw [← s.w (line j), parallelFamily_map_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = s.ι.app zero

Tactic:
by
  rw [← s.w (line j), parallelFamily_map_left]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
H : C
hH : ObjectProperty.singleton G H
h : H ⟶ Y
⊢ ∃! h', h' ≫ f = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
      exact hf h

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
H : C
hH : ObjectProperty.singleton G H
h : X ⟶ H
⊢ ∃! h', f ≫ h' = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
      exact hf h

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : AddCommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
by
        intros
        ext
        dsimp [ConcreteCategory.homEquiv]
        rw [← FreeAbelianGroup.lift_comp]
        rfl

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ Order.pred^[(b - a).toNat] b = a

Tactic:
pred_iterate,

Goal state after:
a b : ℤ
h : a ≤ b
⊢ b - ↑(b - a).toNat = a
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 : ℤ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq : ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b

Tactic:
rcases a with ⟨a, a_le, e1⟩

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : i.range ≤ a.domain
e1 : ∀ (m : M), f m = ↑a ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
⊢ m ≠ n → (fun x y ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m n

Tactic:
hmn

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
⊢ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1)) ⊆ ∅
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
⊢ m ≠ n → (fun x y ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m n

Tactic:
hmn

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
⊢ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1)) ⊆ ∅
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case neg.refine_1
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ 1 < a

Tactic:
contrapose! hpa

Goal state after:
case neg.refine_1
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
hpa : a ≤ 1
⊢ p ∣ a
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop

case inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
rw [← Filter.eventually_forall_le_atBot] at h_evtl

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' : a = 0
⊢ a = b

Tactic:
rw [h', ha']

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 : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - n • p

Tactic:
rw [← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc, toIcoMod]

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

Goal state before:
pp: 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 ∧ s ∈ g (s✝ i)

Tactic:
exact hf.exists_iff fun t₁ t₂ ht H => gm ht H

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

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

Tactic:
by
  simpa only [one_zsmul] using toIocMod_sub_zsmul hp a b 1

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t ∩ closure[inst✝] s

Tactic:
by rw [hs.closure_eq, inter_univ]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s ⊆ s ↔ IsClosed s

Tactic:
rw [frontier, sdiff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]

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

Tactic:
by
  rw [← neg_sub, toIcoMod_neg, neg_zero]

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

Goal state before:
pp: case H.H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝³ z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝³ z✝² ≤ toIocMod ⋯ z✝³ z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝² ≤ toIocMod ⋯ z✝¹ z✝³
h₂₃₄ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝ ≤ toIocMod ⋯ z✝¹ z✝²
⊢ toIcoMod ⋯ z✝³ z✝ ≤ toIocMod ⋯ z✝³ z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝ ≤ toIocMod ⋯ z✝¹ z✝³

Tactic:
apply toIxxMod_trans _ h₁₂₃ h₂₃₄

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace (X × X)
⊢ 𝓝ˢ (diagonal X) = ⨆ x, 𝓝 (x, x)

Tactic:
rw [nhdsSet, ← range_diag, ← range_comp]
  rfl

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.sUnion
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) s
ih : ∀ s ∈ S✝, s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ

Tactic:
| sUnion _ _ ih =>

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
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ coinduced (g ∘ f) inst✝² ≤ coinduced g inst✝¹

Tactic:
← coinduced_compose,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ coinduced g (coinduced f inst✝²) ≤ coinduced g inst✝¹
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case e_h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ closure[inst✝] ∘ image f = image f ∘ closure[inst✝¹]

Tactic:
ext s : 1

Goal state after:
case e_h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
s : Set X
⊢ (closure[inst✝] ∘ image f) s = (image f ∘ closure[inst✝¹]) s
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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ (map f (F.lift' closure[inst✝¹]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst✝¹] ⊓ comap f (𝓟 {y})).NeBot

Tactic:
← map_neBot_iff f,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ (map f (F.lift' closure[inst✝¹]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst✝¹] ⊓ comap f (𝓟 {y}))).NeBot
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Goal state after:
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : s ×ˢ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ ((IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)) → IsClosedMap f

Tactic:
rintro h Z hZ

Goal state after:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[instTopologicalSpaceSum] Z
⊢ IsClosed[inst✝] (f '' Z)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
⊢ SeparableSpace α

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : IsEmpty α
⊢ SeparableSpace α

case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
⊢ SeparableSpace α
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
α : ι → Type u_3
s : (i : ι) → Set (α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable {f | ∀ (i : ι), f i ∈ s i}

Tactic:
simpa only [← mem_univ_pi] using! IsSeparable.univ_pi h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ f '' s ⊆ closure[inst✝] (f '' c)

Tactic:
rw [image_subset_iff]

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ s ⊆ f ⁻¹' closure[inst✝] (f '' c)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsClosed[instTopologicalSpaceSigma] s ↔ ∀ (i : ι), IsClosed[inst✝ i] (Sigma.mk i ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sigma_iff, preimage_compl]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]
  simp only [← range_sigmaMk]
  exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (𝓝 x) = comap f (𝓝 (f ⟨i, x⟩))

Tactic:
(h₁ i).nhds_eq_comap,

Goal state after:
case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (comap (f ∘ Sigma.mk i) (𝓝 ((f ∘ Sigma.mk i) x))) = comap f (𝓝 (f ⟨i, x⟩))
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
let b := ⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' countableBasis (E i)
  have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
  have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
  exact A.secondCountableTopology B

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
⊢ y ∈ U → IsOpen[inst✝] U → ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U

Tactic:
y_in_U

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
⊢ IsOpen[inst✝] U → ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
simp only [← nhdsWithin_univ] at hf

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
s : Set α
t : Set ↑s
⊢ Lean.Internal.coeM t = Subtype.val '' t

Tactic:
change ⋃ (x ∈ t), {x.1} = _
  ext
  simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂ i, ↑i).Nonempty

Tactic:
refine hs.inter_iInter_nonempty _ (fun i ↦ ht _ i.2) fun a ↦ ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset ↑t
⊢ (s ∩ ⋂ i ∈ a, ↑i).Nonempty
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
← stableUnderSpecialization_compl_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization sᶜ → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∈ (interior {a | p a})ᶜ
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))

Tactic:
← closure_compl

Goal state after:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∈ closure[inst✝²] {a | p a}ᶜ
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))
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
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
rw [← range_inl_union_range_inr]

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
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (range Sum.inl ∪ range Sum.inr)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ ∃ u, IsOpen[inst✝] u ∧ u ∩ S = s

Tactic:
exact ⟨Uᶜ, isOpen_compl_iff.mpr Uo, by rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
w✝ : Set X
rp : IsClosed[inst✝] w✝
rt : w✝ ∩ t = s
⊢ IsClosed[inst✝] s

Tactic:
← rt

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
w✝ : Set X
rp : IsClosed[inst✝] w✝
rt : w✝ ∩ t = s
⊢ IsClosed[inst✝] (w✝ ∩ t)
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
hst : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢
  exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

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

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) (𝓟 (Iic a))
hbot : IsBot a
⊢ False

Tactic:
disjoint_principal_right

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
⊢ 𝓝[<] a = ⊥

Tactic:
by
  if h : IsMin a then simp [h.Iio_eq]
  else exact (Order.pred_covBy_of_not_isMin h).nhdsLT

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

Goal state before:
pp: α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ 𝓝 a = pure a

Tactic:
rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]

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
⊢ R1Space X

Tactic:
rw [inf_eq_iInf]
  apply R1Space.iInf
  simp [*]

Goal state after: