mathlib-initiative/mathlib-tactics huggingface dataset:
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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
this : HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)

Tactic:
exact hasLimit_of_equivalence_comp (asEquivalence Φ)

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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.map f.unop).app (op (unop Y)))) { down := 𝟙 (unop Y) }) =
    (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.obj (unop X)).map f)) { down := 𝟙 (unop X) })

Tactic:
simp [uliftYoneda]

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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ (hom ((uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j).app (op (unop X)))) { down := 𝟙 (unop X) } =
    (hom ((s.ι.app j).app X)) x

Tactic:
simp [uliftYoneda]

Goal state after:
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
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
eq₁ : uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd = uliftYonedaEquiv.symm y.snd
eq₂ :
  (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) })) =
    (hom ((G.obj P).map (F.map (↑f).unop).op))
      ((hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst)))))
        ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (F.1 (unop x.fst)) }))
eq₃ :
  (hom ((φ.app (unop x.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) ≫ F.map (↑f).unop } =
    (hom ((G.map (uliftYoneda.{max w v₂, v₁, u₁}.map (↑f).unop)).app (op (F.1 (unop y.fst)))))
      ((hom ((φ.app (unop y.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) })
eq₄ :
  ∀ (x_1 : ToType (ULift.{max v₁ w, v₂} (F.obj (unop x.fst) ⟶ F.obj (unop x.fst)))),
    (hom ((φ.app (unop x.fst)).app (op (F.obj (unop y.fst))))) { down := F.map (↑f).unop ≫ x_1.down } =
      (hom ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.fst))).map (F.map (↑f).unop).op))
        ((hom ((φ.app (unop x.fst)).app (op (F.obj (unop x.fst))))) x_1)
⊢ (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((φ.app (unop x.fst)).app (op (F.obj (unop y.fst))))) { down := F.map (↑f).unop ≫ 𝟙 (F.1 (unop x.fst)) }) =
    (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop y.fst))))) { down := 𝟙 (F.1 (unop y.fst)) ≫ F.map (↑f).unop })

Tactic:
simp [uliftYoneda]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Tactic:
refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ (fun h' ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this
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
⊢ (natTrans φ).app (uliftYoneda.{max w v₂, v₁, u₁}.obj X) = (compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X

Tactic:
dsimp [natTrans]
  apply (F.op.lan.obj (uliftYoneda.obj X)).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app _)
  rw [Functor.descOfIsLeftKanExtension_fac]
  apply uliftYonedaEquiv.injective
  rw [uliftYonedaEquiv_presheafHom_uliftYoneda_obj]
  exact _root_.congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ c.ι.app b ≫ g ≫ u = c.ι.app b ≫ g ≫ v

Tactic:
simpa using! huv (f b.as) (by simp) (c.inj _ ≫ g)

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

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ b - (b - a) = a

Tactic:
sub_sub_cancel

Goal state after:
a b : ℤ
h : a ≤ b
⊢ a = a
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ (n + 1).negOnePow = -n.negOnePow

Tactic:
by
  rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : ∀ f ∈ g :: l, Periodic f c
⊢ Periodic (g :: l).prod c

Tactic:
rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (↑n * c - x) = f (-x)

Tactic:
by
  simpa only [sub_eq_neg_add] using h.nat_mul n (-x)

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

Goal state before:
pp: n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0)

Goal state after:
case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = #({k ∈ range n | n.gcd k = 0})

case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
eventually_atTop

Goal state after:
c d : ℕ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → c ^ b < (b - d)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
    Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]
  exact prod_pos (fun p => pos_of_mem_primeFactors)

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

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)

Tactic:
by apply mul_mul_mul_comm

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 - (b - toIcoDiv hp a b • p) = toIcoDiv hp a b • p

Tactic:
sub_sub_cancel

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p = toIcoDiv hp a b • p
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 - (b - toIocDiv hp a b • p) = toIocDiv hp a b • p

Tactic:
sub_sub_cancel

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p = toIocDiv hp a b • p
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Sort v
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
ho : ∀ (i : ι), p i → IsOpen (s i)
i : ι
hi : p i
⊢ interior (s i) ∈ l

Tactic:
by
    simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
⊢ interior (frontier s) = ∅

Tactic:
have A : frontier s = s \ interior s := h.frontier_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in 𝓝 x, x ∈ s i

Tactic:
by
  simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]
  exact ⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
⊢ interior (frontier s) = ∅

Tactic:
by
  have A : frontier s = s \ interior s := h.frontier_eq
  have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono sdiff_subset
  have C : interior (frontier s) ⊆ frontier s := interior_subset
  have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) :=
    subset_inter B (by simpa [A] using C)
  rwa [inter_sdiff_self, subset_empty_iff] at this

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst✝¹, inst✝] g
⊢ DenseRange (g ∘ f)

Tactic:
DenseRange,

Goal state after:
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst✝¹, inst✝] g
⊢ Dense (range (g ∘ f))
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
← neg_sub x₁ x₃,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (-(x₁ - x₃)) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
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:
by
  rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]

Goal state after:
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : C
⊢ x ∈ g ⁻¹' q '' V ↔ x ∈ U

Tactic:
obtain ⟨x, rfl⟩ := hp x

Goal state after:
case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ g ⁻¹' q '' V ↔ p x ∈ U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ DenseRange f ↔ Surjective f

Tactic:
DenseRange,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ Dense (range f) ↔ Surjective f
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]
  simp only [isOpen_coinduced, subset_def, mem_ofPred_eq]

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
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w))

Tactic:
rw [nhds_prod_eq, 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
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x ↦ f (g x, h x)) x

Tactic:
rw [← e] at hf

Goal state after:
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
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x ↦ f (g x, h x)) x
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ DenseRange (Pi.map f)

Tactic:
DenseRange,

Goal state after:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (range (Pi.map f))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst✝¹] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst✝] t
⊢ IsOpen[inst✝¹] (f ⁻¹' t)

Tactic:
by
  convert! (continuousOn_open_iff hs).mp h t ht
  rw [inter_comm, inter_eq_self_of_subset_left hp]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ DenseRange (inclusion hst) ↔ t ⊆ closure[inst✝] s

Tactic:
DenseRange,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ Dense (range (inclusion hst)) ↔ t ⊆ closure[inst✝] s
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 α
x : α
g : β → γ
y : β
hg : ContinuousAt g y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy; exact hg.comp_continuousWithinAt hf

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x ↦ f (g x, h x)) s x

Tactic:
rw [← e] at hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x ↦ f (g x, h x)) s x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : 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 t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ I u, (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I).pi u ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩

Goal state after:
case refine_1
ι : 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 : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ I u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : 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 u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩

Goal state after:
case refine_2
ι : 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 t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩

Goal state after:
case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ range id ∈ f

Tactic:
rw [range_id]; exact univ_mem

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous[inst✝¹, inst✝] f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ Continuous[⨆ i, coinduced (Sigma.mk i) (inst✝¹ i), inst✝] f ↔ ∀ (i : ι), Continuous[inst✝¹ i, inst✝] fun a ↦ f ⟨i, a⟩

Tactic:
rw [continuous_iSup_dom]

Goal state after:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst✝¹ i), inst✝] f) ↔
    ∀ (i : ι), Continuous[inst✝¹ i, inst✝] fun a ↦ f ⟨i, a⟩
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
rw [hx]

Goal state after:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
choose K hcomp hcov using fun i ↦ hcomp i

Goal state after:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ IsSigmaCompact (⋃ i, s i)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst✝] sᶜ)

Tactic:
by
  refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨t, ⟨htcl, htco⟩, hst⟩
    exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl
  · exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ sSup (𝓝 '' s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y

Tactic:
sSup_image,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ a ∈ s ×ˢ t, 𝓝 a = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y