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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).inv.unop ≫ coprod.inl.unop = prod.fst

Tactic:
rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst✝ : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ h.isoLimit.inv ≫ (CostructuredArrow.left E).map g.hom ≫ (CostructuredArrow.hom E).app g.right =
    limit.π (StructuredArrow.proj Y L ⋙ F) g

Tactic:
simpa using! h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
⊢ map₁ (η ≫ μ) = map₁ μ ∘ map₁ η

Tactic:
ext; all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
⊢ map₂ F (𝟙 X) = id

Tactic:
ext; all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ map₂ F (f ≫ g) = map₂ F f ∘ map₂ F g

Tactic:
ext; all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ map₂ G f (map₁ η p) = map₁ η (map₂ F f p)

Tactic:
ext; all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₁) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁))) ≫
      (L ⋙ L.pointwiseLeftKanExtension F).map f

Tactic:
simp only [comp_map,
      pointwiseLeftKanExtension_map, colimit.ι_desc, CostructuredArrow.map_mk]
    rw [id_comp]
    let φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) :=
      CostructuredArrow.homMk f
    exact colimit.w (CostructuredArrow.proj L (L.obj X₂) ⋙ F) φ

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
let β : L.pointwiseLeftKanExtension F ⟶ G :=
    { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }
  have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
      (pointwiseLeftKanExtensionUnit L F) G α = β := by
    apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
    aesop
  exact NatTrans.congr_app h Y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
⊢ A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map f ≫ g)).down

Tactic:
by
  have := (g.naturality_apply f.op) (ULift.up (𝟙 Y))
  dsimp [uliftYonedaEquiv, uliftYoneda] at this ⊢
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
⊢ (∃ a, P a ∧ ∃ b, mk b = X) → P X.right

Tactic:
by rintro ⟨_, h, _, rfl⟩; exact h

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ (∃ a, P a ∧ ∃ b, mk b = X) → P X.left

Tactic:
by rintro ⟨_, h, _, rfl⟩; exact h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
⊢ a = default

Tactic:
let E := equalizer a (i ≫ Classical.choice (hT _))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
⊢ a = default
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)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj X =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      X

Tactic:
cases X <;> rfl

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)
X : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      X =
    (𝟭 WalkingParallelPair).obj X

Tactic:
cases X <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D

Tactic:
exact HasSeparator.of_equivalence α

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y : (Discrete.functor F).obj { as := i }
⊢ ∃ i_1 y_1, c.inj i_1 y_1 = c.ι { as := i } y

Tactic:
exact ⟨i, y, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
x : c.pt
⊢ ∃ i y, c.inj i y = x

Tactic:
obtain ⟨⟨i⟩, y, rfl⟩ := hc.ι_jointly_surjective x
  exact ⟨i, y, rfl⟩

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b))

Tactic:
abel

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

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

pp: case mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a

Tactic:
· intro hap b h; rcases h with ⟨_, rfl⟩
            exact hap (dvd_mul_left _ _)

Goal state after:
case mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
set xs : ℕ → α := fun n => (List.range n).foldl (fun x n ↦ c x (ys n)) (ys 0)

Goal state after:
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
  contrapose! H
  have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
  rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
  rw [tendsto_inf, tendsto_principal] at hx
  refine ⟨x, hx.1, fun h => ?_⟩
  rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩
  exact hnotMem hmem

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 : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p

Tactic:
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 : α
m : ℤ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
by
  rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, 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 : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p

Tactic:
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 : α
⊢ -b - -(toIocDiv hp (-a) b • p + 1 • p) = p - (b - toIocDiv hp (-a) b • p)

Tactic:
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 : α
⊢ -b - -(toIcoDiv hp (-a) b • p + 1 • p) = p - (b - toIcoDiv hp (-a) b • p)

Tactic:
abel

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

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

Tactic:
abel

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

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

Tactic:
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 : α
⊢ toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
rw [← not_exists, not_imp_not]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s V : Set X
⊢ s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x

Tactic:
subset_def,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s V : Set X
⊢ (∀ x ∈ s, x ∈ interior V) ↔ ∀ x ∈ s, V ∈ 𝓝 x
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ {x | 𝓝 x ≤ 𝓟 s} ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Tactic:
subset_def,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ x ∈ s, x ∈ {x | 𝓝 x ≤ 𝓟 s}) ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen[inst✝] i ∧ s ⊆ i) ∧ i ⊆ t

Tactic:
simp [mem_nhdsSet_iff_exists, and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p

Tactic:
abel

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p

Tactic:
abel

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 : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
hf.isOpen_preimage

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] s
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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst✝¹] (g ⁻¹' s) ↔ IsOpen[inst✝²] (f ⁻¹' g ⁻¹' s)

Tactic:
hf.isOpen_preimage

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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst✝¹] (g ⁻¹' s) ↔ IsOpen[inst✝¹] (g ⁻¹' s)
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap (f ∘ id)

Tactic:
← h.self_comp_symm,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap (f ∘ ⇑h ∘ ⇑h.symm)
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
⊢ IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
by
  rw [isClosedMap_iff_comap_nhdsSet_le]
  constructor
  · exact fun H y ↦ nhdsSet_singleton (x := y) ▸ H
  · intro H s
    rw [← Set.biUnion_of_singleton s]
    simp_rw [preimage_iUnion, nhdsSet_iUnion, comap_iSup, nhdsSet_singleton]
    exact iSup₂_mono fun _ _ ↦ H

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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
⊢ Sort ?u.37

Tactic:
haveI := tb2

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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.37
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
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s

Tactic:
preimage_compl,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ (f ⁻¹' f '' sᶜ)ᶜ = s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {↑x}ᶜ] x = ⊥

Tactic:
preimage_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {↑x})ᶜ] x = ⊥
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n : ℕ
hn : ∃ m, accumulate s n ⊆ s m
⊢ ∃ m, accumulate s (n + 1) ⊆ s m

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case pos
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
use t i

Goal state after:
case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ (fun a ↦ if a ∈ I then t a else univ) i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.smallSets = generate (powerset '' f.sets)

Tactic:
generate_eq_biInf,

Goal state after:
α : Type u_1
f : Filter α
⊢ f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds.inl
α : 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.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inl '' v, mem_union_left _ (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
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
    rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
    refine ⟨t, ?_⟩
    rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
have : ∀ f : Filter X, f ⊓ l = comap Function.diag (f ×ˢ l) := fun f ↦ by
    simpa only [comap_prod] using! congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap Function.diag (f ×ˢ l)
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
this : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x
⊢ IsBounded (f '' s)

Tactic:
exact ((isBounded_biUnion_finset I).2 fun i _ => (hU i).2).subset (this ▸ Set.image_mono hI.2)

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, Subtype.forall] using hst

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
⊢ x = y

Tactic:
rcases h x y hxy with ⟨s, hxs, hys, hs⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y