mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
    rw [this]
    infer_instance
  ext X
  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]
  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩

Goal state after:
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 : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ mk q ≅ P

Tactic:
fapply isoMk
        · exact Subobject.underlyingIso _
        · exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)

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)
inst✝ : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
by rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]

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

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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ ∀ {a b : Subobject (op A)},
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
apply Subobject.ind₂
    intro P Q f g hf hg
    refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩
    · refine (homMk (Subobject.ofMkLEMk _ _ h).unop ((cancel_epi (S.map g.unop.left)).1 ?_)).op
      dsimp
      simp only [← S.map_comp_assoc, unop_left_comp_ofMkLEMk_unop, unop_op, CommaMorphism.w,
        right_eq_id, Functor.const_obj_map]
    · apply Quiver.Hom.unop_inj
      ext
      exact unop_left_comp_ofMkLEMk_unop _
    · refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_
      refine Quiver.Hom.unop_inj ?_
      have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
      simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk_obj, Over.mk_left,
        MonoOver.mk_arrow, unop_comp, Quiver.Hom.unop_op, comp_left]
          using congr_arg CommaMorphism.left this

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 : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ (u ≫ g) ≫ c.π.app b = (v ≫ g) ≫ c.π.app b

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

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    (AddCommGrpCat.Hom.hom f) ((AddCommGrpCat.Hom.hom h) { down := x }) =
      (AddCommGrpCat.Hom.hom g) ((AddCommGrpCat.Hom.hom h) { down := x })
x : ↑A
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
specialize h (AddCommGrpCat.ofHom
    (AddMonoidHom.mk' (fun y => y • x) fun y z => by simp only [add_smul])) 1

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
x : ↑A
h :
  (AddCommGrpCat.Hom.hom f)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 }) =
    (AddCommGrpCat.Hom.hom g)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 })
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : (sigma F).inj x✝² x✝¹ = (sigma F).inj x✝² x✝
⊢ x✝¹ = x✝

Tactic:
by rw [Sigma.ext_iff] at h; simpa using h

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

Goal state before:
pp: case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono (free.map f)

Tactic:
· have hf : Function.Injective f := by rwa [← mono_iff_injective]
      obtain ⟨g, hg⟩ := hf.hasLeftInverse
      have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }
      infer_instance

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

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ g (n • ⟨m, ⋯⟩) = g ⟨n • m, hn⟩

Tactic:
SetLike.mk_smul_mk

Goal state after:
case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ g ⟨n • m, ⋯⟩ = g ⟨n • m, hn⟩
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case domain_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
⊢ x✝ ∈ x✝³.domain ↔ x✝ ∈ x✝².domain

Tactic:
congr!

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

Goal state before:
pp: case to_fun_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
ha✝ : x✝ ∈ x✝³.domain
hb✝ : x✝ ∈ x✝².domain
⊢ ↑x✝³.toLinearPMap ⟨x✝, ha✝⟩ = ↑x✝².toLinearPMap ⟨x✝, hb✝⟩

Tactic:
congr!

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ b ≡ a [PMOD p] ↔ ↑a = ↑b

Tactic:
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]

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
⊢ m = Exists.choose ⋯

Tactic:
exact Fact.out (p := Function.Injective i)
          (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm

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

Goal state before:
pp: n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩

Goal state after:
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ ↑(range n)
⊢ n.gcd x ∣ n
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 : α
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
by
  suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
  rw [← neg_eq_iff_eq_neg, eq_comm]
  apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
  obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)
  rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho
  rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc
  refine ⟨ho, hc.trans_eq ?_⟩
  rw [neg_add, neg_add_cancel_right]

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 (p + a) b = p + toIcoMod hp a b

Tactic:
by
  rw [add_comm, toIcoMod_add_right', add_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 c : α
h : toIcoMod hp a b = toIcoMod hp a c
| c - b

Tactic:
← toIcoMod_add_toIcoDiv_zsmul hp a b,

Goal state after:
α : 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
| c - (toIcoMod hp a b + toIcoDiv hp a b • p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t

Tactic:
simp [interior]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (interior s) (frontier s)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s ∩ frontier s = ∅
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)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| b

Tactic:
← toIcoMod_add_toIcoDiv_zsmul hp a b,

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)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| toIcoMod hp a b + toIcoDiv hp a b • p
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ x, ∃ (_ : x ∈ s), x ∈ t

Tactic:
exists_prop

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

Goal state before:
pp: case right
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
not_le

Goal state after:
case right
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₂
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ toIocMod hp x₃ x₂ < toIcoMod hp x₃ x₄
⊢ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₄
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 + p - b < ↑⌊(a + p - b) / p⌋ * p + p

Tactic:
add_comm (_ * _),

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

Goal state before:
pp: α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a = n a

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ n a

case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := ⋯
⊢ n a ≤ 𝓝 a
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
let := TopologicalSpace.coinduced π ‹_›

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ pure a ⊔ f

case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ pure a ⊔ f ≤ 𝓝 a
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsClosed[inst✝] s
⊢ ∃ c, IsClosed[inst✝¹] c ∧ f '' s = c ∩ range f

Tactic:
by
  obtain ⟨c, hc, rfl⟩ := hf.isClosed_iff.1 hs
  exact ⟨c, hc, image_preimage_eq_inter_range⟩

Goal state after:
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 : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap ((⇑h.symm ∘ ⇑h) ∘ f)

Tactic:
Function.comp_assoc

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 : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap (⇑h.symm ∘ ⇑h ∘ f)
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
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (𝓝ˢ s) = 𝓝ˢ (f '' s)

Tactic:
by
  rw [← biUnion_of_singleton s]
  simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite

Tactic:
isOpen_mk,

Goal state after:
X : Type u
s : Set (CofiniteTopology X)
⊢ (WithTopology.toTopology
            { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) ≤ 𝓝[g '' s] g x

case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ (∃ i, ∃ (_ : i ≤ x), z ∈ s i) ↔ ∃ y ≤ x, z ∈ s y

Tactic:
exists_prop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_1
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ hF.toFinset, U i ∈ T i

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Goal state after:
case refine_2.refine_1
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, U i ∈ T i
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ a ∈ ⋂ i ∈ hF.toFinset, U i

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Goal state after:
case refine_2.refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, a ∈ U i
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ hF.toFinset, U i ⊆ u

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Goal state after:
case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Tactic:
by
  let _ := ⨅ i, t i
  refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
  · rintro - ⟨U, F, hU, rfl⟩
    refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)
  · intro a u ha hu
    rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
    refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]
    · exact fun i hi ↦ (hU i hi).1
    · exact fun i hi ↦ (hU i hi).2
    · exact hUu

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case right
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ t = generateFrom (range (uncurry b))

Tactic:
apply le_antisymm

Goal state after:
case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ t ≤ generateFrom (range (uncurry b))

case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ generateFrom (range (uncurry b)) ≤ t
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_antisymm

Goal state after:
case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)

case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : 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
⊢ ContinuousOn g (⋃ i, f i)

Tactic:
rintro x -
  rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
  intro i
  by_cases hx : x ∈ closure (f i)
  · exact hc i _ hx
  · rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
    rw [hx]
    exact tendsto_bot

Goal state after: