mathlib-initiative/mathlib-tactics huggingface dataset:
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.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
⊢ f₁ = f₂

Tactic:
ext Y

Goal state after:
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.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y
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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
⊢ f₁ = f₂

Tactic:
ext Y

Goal state after:
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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ f₁.left.app Y = f₂.left.app Y
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ unitForward μ X (YonedaCollection.map₁ (restrictedYonedaObjMap₁ ε hε) p) =
    (ConcreteCategory.hom (ε.app (op X))) (unitForward η X p)

Tactic:
simp [unitForward]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X Y : C
f : X ⟶ Y
p : YonedaCollection (restrictedYonedaObj η) Y
⊢ unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) =
    (ConcreteCategory.hom (F.map f.op)) (unitForward η Y p)

Tactic:
simp [unitForward]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

Tactic:
simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]

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✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
φ : Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X) ⟶ Y
⊢ uliftYonedaEquiv (StructuredArrow.Hom.right φ) =
    uliftYonedaEquiv
      (StructuredArrow.Hom.right
        (StructuredArrow.homMk (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) ⋯))

Tactic:
simp [← StructuredArrow.w φ, uliftYonedaEquiv, uliftYonedaMap]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ t = i ≫ h

Tactic:
ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ t = t
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case i
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ op (mk q) ≅ P

Tactic:
refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
        · exact (Subobject.underlyingIso f.unop.left.op).unop
        · refine (cancel_epi (S.map f.unop.left)).1 ?_
          simpa [← Category.assoc, ← S.map_comp] using hq

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
⊢ Epi (lim.map f)

Tactic:
let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
⊢ Epi (lim.map f)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ IsColimit (coconeπOpCompShrinkYonedaObj F X)

Tactic:
refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)
  · let G := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj X
    let c := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
    have (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = x) :
        G.ιColimitType (op (elementsMk _ _ x))
          (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u := by
      obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
      obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
      dsimp [c] at v h
      simp only [Equiv.apply_symm_apply] at h
      rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
      simp [G, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]
    intro u₁ u₂ hu
    generalize hx₁ : G.descColimitType c u₁ = x
    have hx₂ : G.descColimitType c u₂ = x := by rw [← hx₁]; exact hu.symm
    rw [← this _ _ hx₁, ← this _ _ hx₂]
  · exact ⟨Functor.ιColimitType _ (op (elementsMk _ _ x))
      (shrinkYonedaObjObjEquiv.symm (𝟙 X)), by simp⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : unop (op u.fst) ⟶ X₁
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd)).toFun
      (shrinkYonedaObjObjEquiv.symm g) =
    (ConcreteCategory.hom ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f)).toFun
      (shrinkYonedaObjObjEquiv.symm g)

Tactic:
simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map (shrinkYonedaObjObjEquiv u.snd)))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd

Tactic:
simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n ^ n) = x

Tactic:
RootableBy.root_cancel _ hn,

Goal state after:
A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f y = x
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 z2 : ↥(ideal i f y)
⊢ ↑(z1 + z2) • y = ↑⟨↑z1 • y, ⋯⟩ + ↑⟨↑z2 • y, ⋯⟩

Tactic:
apply add_smul

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
⊢ ∀ (n : ℕ), motive n

Tactic:
by
  refine recOnPrimePow zero one ?_
  rintro a p n hp - - ha
  induction n with
  | zero => simpa using ha
  | succ n ih =>
    rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih

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

Goal state before:
pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Tactic:
· rintro rfl
      rw [totient_one, tsub_self] at h
      exact one_ne_zero h

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot atBot

Tactic:
by
  rw [← prod_atBot_atBot_eq]
  exact tendsto_id.prodMk tendsto_id

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - (b + ↑⌊(a + p - b) / p⌋ * p)

Tactic:
sub_add_eq_sub_sub

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - b - ↑⌊(a + p - b) / p⌋ * p
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : IndiscreteTopology α
x : α
f : Filter α
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
simpa [ClusterPt, IndiscreteTopology.nhds_eq]

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 : IsOpenMap f
s : Set Y
⊢ (closure[inst✝¹] (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure[inst✝] s)ᶜ

Tactic:
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] ↑a, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J

Tactic:
nhdsWithin_eq_map_subtype_coe (hst a.prop),

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in map Subtype.val (𝓝 ⟨↑a, ⋯⟩), ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
s : Set (CofiniteTopology X)
⊢ s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite

Tactic:
by simp [nhds_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)

Tactic:
rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous[inst✝², inst✝] f ∧ Injective f ∧ IsOpenMap f
hg : Continuous[inst✝¹, inst✝] g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst✝] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousAt f x

Tactic:
by
  rw [← continuousWithinAt_compl_self]
  exact continuousWithinAt_of_not_accPt h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (𝓝 x.1 ×ˢ pure x.2 ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
prod_pure,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (fun a ↦ (a, x.2)) (𝓝 x.1) ⊓ 𝓟 s) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsClosed[inst✝] (s ∩ t)

Tactic:
by simpa using hs.isClosedMap_subtype_val _ h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map f (𝓝 a ×ˢ pure b)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)

Tactic:
prod_pure,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map f (map (fun a ↦ (a, b)) (𝓝 a))) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.cons (f i_1) (g i_1) i.succ) l (𝓝 (Fin.cons x y i.succ))

Tactic:
by simpa using tendsto_pi_nhds.1 hg

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n), Tendsto (fun i_1 ↦ i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))

Tactic:
by simpa using tendsto_pi_nhds.1 hg

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ

Tactic:
refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) → ∃ n, s n = univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
rw [← continuousOn_univ, ← hs']
  exact ContinuousOn.iUnion_of_isOpen hf hs

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ i, s i) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
⊢ ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f

Tactic:
by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ i ∈ t, f ↑i
⊢ x ∈ ⋃ y ∈ t, f ↑y

Tactic:
exact htU ⟨x, hx⟩

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
⊢ (do
      let a ← γ
      pure ↑a) ⊆
    β

Tactic:
intro _

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
a✝ : α
⊢ (a✝ ∈ do
      let a ← γ
      pure ↑a) →
    a✝ ∈ β
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Tactic:
simp [-sdiff_singleton]

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
s t : UpperSet α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by cases s; cases t; congr

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
· refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hab⟩
    exact hat <| hst _ ha _ hb hab

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∃ i, a ∈ f i

Tactic:
coe_iInf

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨅ i, f i).compl = ↑(⨅ i, (f i).compl)

Tactic:
simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)
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
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X

Tactic:
rw [cocompact_eq_cofinite X]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ IsPreirreducible s

Tactic:
(Lean.cdot
 (Lean.cdotTk "·")
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.intro "intro" [`u `v `hu `hv `hu' `hv'])
    []
    (Tactic.simpa
     "simpa"
     []
     []
     (Tactic.simpaArgsRest
      (Tactic.optConfig [])
      []
      []
      [(Tactic.simpArgs "[" [(Tactic.simpStar "*")] "]")]
      ["using"
       (Term.app
        `h
        [(choice
          («term{_}» "{" [`u "," `v] "}")
          (Term.structInst
           "{"
           []
           (Term.structInstFields
            [(Term.structInstField (Term.structInstLVal `u []) [])
             ","
             (Term.structInstField (Term.structInstLVal `v []) [])])
           (Term.optEllipsis [])
           []
           "}"))])]))])))

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
exact hb.filter_mono nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n n, r i (succ i)) → ReflTransGen r n n

Tactic:
intro _

Goal state after:
case refine_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
h✝ : ∀ i ∈ Ico n n, r i (succ i)
⊢ ReflTransGen r n n
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}

Tactic:
← nhdsWithin_univ,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[univ] x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
⊢ False

Tactic:
rcases this.exists_lt with ⟨y, hyx, hys⟩

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
y : α
hyx : y < x
hys : y ∈ s
⊢ False