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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ uliftYonedaEquiv (presheafHom φ (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) =
    uliftYonedaEquiv
      (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X) ≫
        F.op.whiskerLeft ((compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X))

Tactic:
uliftYonedaEquiv_presheafHom_uliftYoneda_obj

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (hom ((φ.app X).app (F.op.obj (op X)))) { down := 𝟙 (unop (F.op.obj (op X))) } =
    uliftYonedaEquiv
      (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X) ≫
        F.op.whiskerLeft ((compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
⊢ x✝ = ↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹))

Tactic:
ext ⟨⟩

Goal state after:
case inl
C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
val✝ : X
⊢ (ConcreteCategory.hom x✝).toFun (Sum.inl val✝) =
    (ConcreteCategory.hom
          (↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹)))).toFun
      (Sum.inl val✝)

case inr
C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
val✝ : Y
⊢ (ConcreteCategory.hom x✝).toFun (Sum.inr val✝) =
    (ConcreteCategory.hom
          (↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹)))).toFun
      (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩

Goal state after:
case mpr.refine_1
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ {T : Type u} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

case mpr.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T), c.inl ≫ ?mpr.refine_1 f g = f

case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T), c.inr ≫ ?mpr.refine_1 f g = g

case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T), c.inl ≫ m = f → c.inr ≫ m = g → m = ?mpr.refine_1 f g
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this : (ConcreteCategory.hom c.inr) x ∈ ⊥
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x

Tactic:
exact this.elim

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (z • Additive.ofMul u) = u ^ z

Tactic:
toMul_zsmul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (Additive.ofMul u) ^ z = u ^ z
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
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    (RingHom.id R) z1 • ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

Tactic:
by
    simp_rw [← (extensionOfMax i f).toLinearPMap.map_smul]
    congr 2
    apply mul_smul

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

Goal state before:
pp: case e_a
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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + (r • y - snd i x • y)

Tactic:
Subtype.coe_mk,

Goal state after:
case e_a
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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + (r • y - snd i x • y)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a

Tactic:
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le

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

Goal state before:
pp: case refine_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S

Tactic:
simp [cond.univ_mem]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun x ↦ x * p) (range (p ^ n))

Tactic:
simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)
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 : α
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a (z • p + b)

Tactic:
toIcoMod_zsmul_add

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

Tactic:
btw_coe_iff',

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ toIcoMod ⋯ 0 (x₂ - x₁) ≤ toIocMod ⋯ 0 (x₃ - x₁) ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst✝] s ↔ x ∈ f ⁻¹' closure[inst✝¹] (f '' s)

Tactic:
rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t

Tactic:
simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)

Tactic:
rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Tactic:
delta nhdsWithin
  rw [← inf_principal, inf_assoc]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
⊢ s ∈ 𝓝 x.1

Tactic:
rcases x with ⟨x, y⟩

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ s ∈ 𝓝 (x, y).1
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)
⊢ s ∈ 𝓝 x.2

Tactic:
rcases x with ⟨x, y⟩

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ s ∈ 𝓝 (x, y).2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed[inst✝] t → ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
have : ∀ t, IsClosed (s.domRestrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isClosed_induced_iff, Set.domRestrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsClosed[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed[inst✝] t → ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ 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
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
this✝ : Nonempty Y
this : Nonempty W
⊢ IsOpenQuotientMap (Prod.map f g) ↔ IsOpenQuotientMap f ∧ IsOpenQuotientMap g

Tactic:
grind [isOpenQuotientMap_iff, continuous_prodMap_iff, isOpenMap_prodMap_iff, Prod.map_surjective]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ (f ⁻¹' v ∩ f ⁻¹' t') ⊆ f ⁻¹' u

Tactic:
← preimage_inter

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
let B := { b ∈ countableBasis α | ∃ i, b ⊆ s i }

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι✝ : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
ι : Type u_4
inst✝² : Finite ι
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (X i)
f : (i : ι) → X i
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 f

Tactic:
choose s hsc hs using fun i ↦ exists_compact_mem_nhds (f i)

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι✝ : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t : Set X✝
ι : Type u_4
inst✝² : Finite ι
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (X i)
f : (i : ι) → X i
s : (i : ι) → Set (X i)
hsc : ∀ (i : ι), IsCompact (s i)
hs : ∀ (i : ι), s i ∈ 𝓝 (f i)
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 f
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
eventually_nhdsSet_iff_forall,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
      exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
rw [← nhdsSet_singleton]
  exact hs.le_nhdsSet_of_clusterPt hmem h

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
replace hK := hK.inter_right hf'

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (f ⁻¹' K)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S

Tactic:
rw [specializes_iff_forall_open]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
⊢ Continuous[_, inst✝] (uncurry (lift₂ f hf)) ↔ Continuous[instTopologicalSpaceProd, inst✝] (uncurry f)

Tactic:
by
  simp only [← continuousOn_univ, continuousOn_lift₂, preimage_univ]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
z : X
⊢ z ∈ t → ∃ t_1 ∈ 𝓝[≠] z, t_1 ∩ (t \ s) = ∅

Tactic:
hz

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
z : X
hz : z ∈ t
⊢ ∃ t_1 ∈ 𝓝[≠] z, t_1 ∩ (t \ s) = ∅
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
⊢ z ∈ s → ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅

Tactic:
hz

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)

Tactic:
simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_sdiff]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure[inst✝¹] K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
by
  refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
  contrapose! hy
  have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
  simpa only [disjoint_iff, notMem_closure_iff_nhdsWithin_eq_bot]
    using! this.mono_right principal_le_nhdsSet

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst✝¹] K = ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
ext; simp [hK.mem_closure_iff_exists_inseparable]

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

Goal state before:
pp: case insert.refine_2.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ update K x K₁ i ⊆ U i

Tactic:
· simp only [update_of_ne hi, h2K]

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

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

Tactic:
obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2

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