mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ k ≫ 0 ≫ l = 0

Tactic:
zero_comp,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ k ≫ 0 = 0
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
h : f.app X ≫ (L.lanUnit.app F₂).app X = (L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)
⊢ f.app X ≫ α.app X =
    ((L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)

Tactic:
← h,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
h : f.app X ≫ (L.lanUnit.app F₂).app X = (L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)
⊢ f.app X ≫ α.app X =
    (f.app X ≫ (L.lanUnit.app F₂).app X) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft e.hom ≫ L.whiskerLeft e.symm.hom = α

Tactic:
← whiskerLeft_comp,

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft (e.hom ≫ e.symm.hom) = α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
⊢ StructuredArrow.IsUniversal b

Tactic:
by
  letI (y : L'.LeftExtension F₁) : Unique (b ⟶ y) := by
    let u : (LeftExtension.precomp₂ L' α).obj b ⟶
      (LeftExtension.precomp₂ L' α).obj y := hb.to _
    refine
      ⟨⟨StructuredArrow.homMk u.right <| by
          apply hα.hom_ext
          ext t
          have := congr_app u.w t
          dsimp at this
          simp only [precomp₂_obj_hom_app, assoc] at this
          simp [this]⟩, fun a => ?_⟩
    ext1
    apply hb.hom_ext
    ext t
    have := congr_app u.w t
    dsimp at this
    simp only [precomp₂_obj_hom_app, assoc] at this
    simp [this, ← a.w]
  apply IsInitial.ofUnique

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X : C
inst✝ : HasCoproduct (P.coproductFromFamily X)
Z✝ : C
u v : X ⟶ Z✝
huv : P.coproductFrom X ≫ u = P.coproductFrom X ≫ v
G : C
hG : P G
h : G ⟶ X
⊢ h ≫ u = h ≫ v

Tactic:
simpa using P.ιCoproductFrom h hG ≫= huv

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).g).ker → x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
(hx : _ = _)

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
hx : (AddCommGrpCat.Hom.hom (S.map colim).g) x = 0
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁴ : (coyoneda.obj (op G)).Faithful
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
hfg : ∀ (h : G ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝
⊢ (coyoneda.obj (op G)).map x✝¹ = (coyoneda.obj (op G)).map x✝

Tactic:
by ext; apply hfg

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁴ : (yoneda.obj G).Faithful
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
hfg : ∀ (h : x✝² ⟶ G), x✝¹ ≫ h = x✝ ≫ h
⊢ (yoneda.obj G).map x✝¹.op = (yoneda.obj G).map x✝.op

Tactic:
by ext; apply hfg

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
· have := h Y
    refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)
    simpa using hh j.as

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
⊢ Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (fromSigma F c)

Tactic:
by
  rw [(isColimit_sigma F).iff_bijective]
  aesop

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

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
rintro ⟨h⟩

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective ⇑(ConcreteCategory.hom c.inl) ∧
    Injective ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ a, (LinearMap.lcomp R M (Submodule.subtype I)) a = g

Tactic:
rcases h I g with ⟨g', hg'⟩
    use g'
    ext x
    simp [hg']

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)
m : M
⊢ f m =
    ↑{ domain := i.range, toFun := { toFun := fun x ↦ f (Exists.choose ⋯), map_add' := ⋯, map_smul' := ⋯ } } ⟨i m, ⋯⟩

Tactic:
by
        simp only [LinearPMap.mk_apply, LinearMap.coe_mk]
        dsimp
        apply congrArg
        exact Fact.out (p := Function.Injective i)
          (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm

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

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = (filter (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a)))).card

Tactic:
← map_count_True_eq_filter_card,

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) = (filter (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a)))).card
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) = (filter (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a)))).card

Tactic:
← map_count_True_eq_filter_card,

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a))))
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:
by
      rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le

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

Goal state before:
pp: case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ False

Tactic:
suffices a.totient < (p * a * d).totient by
    rw [← mul_assoc, mul_comm a] at h'
    exact h'.not_lt this

Goal state after:
case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (p * a * d)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
← h,

Goal state after:
case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : φ a = φ (2 * a)
ha' : ¬a = 0
h : 2 * a = b
⊢ False
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
ι : Sort v
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (s i)ᶜ
⊢ IsOpen[inst✝¹] (⋂ i, (s i)ᶜ)

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

Tactic:
← h,

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

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s

Tactic:
· rintro U U_op ⟨x, x_in⟩
    exact mem_closure_iff.1 (h _) U U_op x_in

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s
Module: Mathlib.Topology.Neighborhoods

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

Tactic:
by simp_rw [interior_eq_nhds, subset_def, mem_ofPred]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
s : Set Y
hs : IsOpen[inst✝] s
⊢ f ⁻¹' s ⊆ interior (f ⁻¹' s)

Tactic:
← h,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
s : Set Y
hs : IsOpen[inst✝] s
⊢ f ⁻¹' s ⊆ f ⁻¹' interior s
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr.inl
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

pp: case mpr.inr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)

Tactic:
· exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩

Goal state after:
case mpr.inr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst✝] (⋂ i ∈ f, {x | x ∈ closure[inst✝] i})

Tactic:
exact isClosed_biInter fun _ _ ↦ isClosed_closure

Goal state after:
Module: Mathlib.Topology.NhdsSet

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

Tactic:
← range_diag,

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace (X × X)
⊢ sSup (𝓝 '' range Function.diag) = ⨆ x, 𝓝 (x, x)
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
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ ClusterPt x (comap f l)

Tactic:
rw [ClusterPt, ← map_neBot_iff, Filter.push_pull]
  exact h.neBot.mono <| inf_le_inf_right _ <| hf.nhds_le _

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
hs : ∀ (s : Set X), closure[inst✝] (f '' s) ⊆ f '' closure[inst✝¹] s
c : Set X
hc : IsClosed[inst✝¹] c
⊢ f '' closure[inst✝¹] c = f '' c

Tactic:
hc.closure_eq

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), closure[inst✝] (f '' s) ⊆ f '' closure[inst✝¹] s
c : Set X
hc : IsClosed[inst✝¹] c
⊢ f '' c = f '' c
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
by
  rw [nhds_prod_eq]
  exact hf.prodMap hg

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
by
  rw [nhds_prod_eq]
  exact hf.prodMap hg

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 → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst✝¹, inst✝] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝², inst✝] fun x ↦ f x y
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
b : Y
hb : b ∈ t
⊢ f x b ∈ closure[inst✝] u

Tactic:
apply map_mem_closure (hf₂ b) hx fun a ha ↦ h a ha b hb

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
x : X
f : Y → Z
⊢ (IsInducing fun x' ↦ (x, f x')) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
have A := (h x (h₁ hx)).mono h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : ContinuousWithinAt f s₁ x
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ Subtype.val '' Subtype.val ⁻¹' closure[inst✝] (Subtype.val '' s ↓∩ t) = Subtype.val '' s ↓∩ t ↔
    s ∩ closure[inst✝] (s ∩ t) ⊆ t

Tactic:
Subtype.image_preimage_coe,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (Subtype.val '' s ↓∩ t) = Subtype.val '' s ↓∩ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (Subtype.val '' s ↓∩ t) = Subtype.val '' s ↓∩ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

Tactic:
Subtype.image_preimage_coe,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst✝] (s ∩ t) = s ∩ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i ↦ f i x) u (𝓝 (g x))

Tactic:
rw [nhds_pi, Filter.tendsto_pi]

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 γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ MapsTo (fun b ↦ (a, b)) sβ (sα ×ˢ sβ)

Tactic:
grind [Set.MapsTo]

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 γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ MapsTo (fun a ↦ (a, b)) sα (sα ×ˢ sβ)

Tactic:
grind [Set.MapsTo]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)

Tactic:
by rwa [image_univ]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
⊢ ContinuousOn f (s ∪ t)

Tactic:
by
  classical
  refine fun x hx ↦ .union ?_ ?_
  · refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [hs.closure_eq]
  · refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [ht.closure_eq]

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 s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ f x✝ ∈ U

Tactic:
← mem_preimage

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ x✝ ∈ f ⁻¹' U
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ 𝓝 x → s ∈ u → x ∈ s

Tactic:
by
  simp [isClosed_iff_clusterPt, ClusterPt, ← exists_ultrafilter_iff]

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

Goal state before:
pp: case mpr.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
this : f '' (f ⁻¹' L n ∩ s) = L n
⊢ IsCompact ((fun n ↦ f ⁻¹' L n ∩ s) n)

Tactic:
apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))

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
y✝ : Y
hf : Tendsto f (cocompact X) (𝓝 y✝)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
⊢ y ∈ t → y ∈ insert y✝ (range f) → y ∈ f '' K

Tactic:
hyt

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y✝ : Y
hf : Tendsto f (cocompact X) (𝓝 y✝)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
⊢ y ∈ insert y✝ (range f) → y ∈ f '' K
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inr.hs
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}) x

Tactic:
have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = s

Tactic:
refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
  · rintro _ ⟨_, _, rfl⟩; exact isClosed_closure
  · conv_rhs => rw [← H.Union_eq]
    simp

Goal state after: