mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)

Tactic:
apply comm2.hom.naturality g

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : f' ≫ 0 = 0
⊢ Epi f'

Tactic:
by rw [hf']; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
⊢ IsIso h.f'

Tactic:
by
  have := hS.epi_f' h
  have := mono_of_mono_fac h.f'_i
  exact isIso_of_mono_of_epi h.f'

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom = Over.Hom.left h₂.hom

Tactic:
rw [← cancel_mono g.arrow, Over.w h₁.hom, Over.w h₂.hom]

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
⊢ (underlyingIso (𝟙 B)).hom = (underlyingIso (𝟙 B)).hom ≫ 𝟙 B

Tactic:
simp only [comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ kernel.ι f = 0

Tactic:
rw [← cancel_mono f, kernel.condition, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit (((evaluation C D).obj k).mapCocone ((prod.functor.obj F).mapCocone c))

Tactic:
change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (((whiskeringLeft C E D).obj F).mapCocone c)

Tactic:
apply evaluationJointlyReflectsColimits
      intro Y
      change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)
      exact isColimitOfPreserves _ hc

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

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (lim.mapCocone c))

Tactic:
constructor
      apply isColimitOfReflects F
      refine (IsColimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesLimitNatIso F).symm)
        ((_ ⋙ lim).mapCocone c) _ ?_) (isColimitOfPreserves _ hc)
      refine Cocone.ext ((preservesLimitNatIso F).symm.app _) fun i ↦ ?_
      simp only [Functor.comp_obj, lim_obj, Functor.mapCocone_pt, isoWhiskerLeft_inv, Iso.symm_inv,
        Cocone.precompose_obj_pt, whiskeringRight_obj_obj, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, NatTrans.comp_app, whiskerLeft_app, preservesLimitNatIso_hom_app,
        Functor.mapCocone_ι_app, Functor.comp_map, whiskeringRight_obj_map, lim_map, Iso.app_hom,
        Iso.symm_hom, preservesLimitNatIso_inv_app, Category.assoc]
      rw [← Iso.eq_inv_comp]
      exact (preservesLimitNatIso F).inv.naturality _

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.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' ↦ f.unop ≫ h' = h) y
⊢ (y.op ≫ f).unop = h.op.unop

Tactic:
by simpa only using! hy

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.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun h' ↦ h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop

Tactic:
by simpa only using! hy

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

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
⊢ ∀ (y₁ y₂ : A ⟶ X), y₁ ≫ f = g → y₂ ≫ f = g → y₁ = y₂

Tactic:
intro l₁ l₂ h₁ h₂

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
l₁ l₂ : A ⟶ X
h₁ : l₁ ≫ f = g
h₂ : l₂ ≫ f = g
⊢ l₁ = l₂
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
⊢ ∀ (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂

Tactic:
intro l₁ l₂ h₁ h₂

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
l₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
⊢ l₁ = l₂
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
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map f ≫
      WalkingParallelFamily.casesOn j ι (ι ≫ f✝ (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f✝ (Classical.arbitrary J)) ≫ (parallelFamily f✝).map f

Tactic:
by
        obtain - | k := f
        · simp
        · simp [w (Classical.arbitrary J) k]

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
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f✝ j₁ ≫ π = f✝ j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ (parallelFamily f✝).map f ≫ WalkingParallelFamily.casesOn j (f✝ (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn i (f✝ (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map f

Tactic:
by
        obtain - | k := f
        · simp
        · simp [w (Classical.arbitrary J) k]

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)
j₁ j₂ : J
t : Trident f
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂

Tactic:
rw [t.app_zero, t.app_zero]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : Epi p
⊢ f = g

Tactic:
rw [← cancel_epi p]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : Epi p
⊢ p ≫ f = p ≫ g
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
x✝ : A
⊢ (if x : 0 = 0 then 1 else ⋯.choose) = 1

Tactic:
by exact dif_pos rfl

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

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = 1 ↔ (Even n₁ ↔ Even n₂)

Tactic:
negOnePow_eq_one_iff

Goal state after:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑k = ↑(n * k) / ↑n
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = (RingHom.id R) r • ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩

Tactic:
rw [← LinearPMap.map_smul]; dsimp

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ φ n = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
multiplicative_factorization φ (@totient_mul) totient_one hn

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ φ (p ^ k)) = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ (p * n) = p * φ n

Tactic:
gcd_eq_left h,

Goal state after:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * φ n * p
⊢ φ (p * n) = p * φ n
Module: Mathlib.Data.Nat.Totient

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

pp: case neg.refine_2
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ (a * p * d)

Tactic:
· rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]
    · exact hp.one_lt
    · exact totient_pos.mpr <| pos_of_ne_zero ha

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

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

Tactic:
by
  simpa only [one_zsmul] using toIcoMod_add_zsmul hp a b 1

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

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

Tactic:
simpa only [one_zsmul] using toIcoMod_sub_zsmul hp a b 1

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 : α
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ n, c - b = n • p

Tactic:
by
  refine ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩
  · conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
    rw [h, sub_smul]
    abel
  · rcases h with ⟨z, hz⟩
    rw [sub_eq_iff_eq_add] at hz
    rw [hz, toIocMod_zsmul_add]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
⊢ WithTopology.instTopologicalSpace α ⊤ = ⊤

Tactic:
rw [WithTopology.topology_eq_induced, induced_top]

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
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))

Tactic:
map_map,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ 𝓝 (f x) = map (f ∘ g) (𝓝 (f 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
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
isClosedMap_iff_closure_image,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (s : Set X), closure[inst✝] (f '' s) ⊆ f '' closure[inst✝¹] s) ↔
    ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x : X
y : Y
⊢ s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Tactic:
rw [nhds_prod_eq, prod_mem_prod_iff]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case insert
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
s : ι → Set α
a : α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hT : 𝓝[⋃ i ∈ s✝, s i] a = ⨆ i ∈ s✝, 𝓝[s i] a
⊢ 𝓝[⋃ i ∈ insert a✝¹ s✝, s i] a = ⨆ i ∈ insert a✝¹ s✝, 𝓝[s i] a

Tactic:
| insert _ _ hT =>

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s : Set α
⊢ 𝓝ˢ[s] {x} = 𝓝[s] x

Tactic:
by
  simp [nhdsSetWithin, nhdsWithin]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝 x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
by
  simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (range (inclusion hst))

Tactic:
by rwa [range_inclusion]

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
by rwa [range_inclusion]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
s : Set α
hs : IsOpen[t] s
⊢ P s

Tactic:
by
  obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs; exact sUnion _ fun b hb ↦ basis _ <| hS hb

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

Goal state before:
pp: case e'_3
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)

pp: case e'_3
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)

Tactic:
· rw [← disjoint_principal_right]
    exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))

Goal state after:
case e'_3
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)
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 : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) univ

Tactic:
exact continuousOn_prod_of_discrete_left

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
use univ

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
apply eq_of_le

Goal state after:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := ⋯
this : f.NeBot
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
⊢ IsClosed[instTopologicalSpaceSigma] (Sigma.mk i '' s)

Tactic:
isClosed_sigma_iff

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
⊢ ∀ (i_1 : ι), IsClosed[inst✝ i_1] (Sigma.mk i_1 ⁻¹' Sigma.mk i '' s)
Module: Mathlib.Topology.Ultrafilter

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

Tactic:
simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : X → Set X
V_nhds : ∀ x ∈ s, V x ∈ 𝓝 x
hV : ∀ x ∈ s, V x ∩ s ⊆ U x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
refine (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : X → Set X
V_nhds : ∀ x ∈ s, V x ∈ 𝓝 x
hV : ∀ x ∈ s, V x ∩ s ⊆ U x
t : Finset X
x✝ : (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, V x
t_sub_s : ∀ x ∈ t, x ∈ s
ht : s ⊆ ⋃ x ∈ t, V x
⊢ s ⊆ ⋃ i ∈ t, V i ∩ s
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
⊢ IsCompact (insert y (range f))

Tactic:
intro l hne hle
  by_cases hy : ClusterPt y l
  · exact ⟨y, Or.inl rfl, hy⟩
  simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
  rcases hy with ⟨s, hsy, t, htl, hd⟩
  rcases mem_cocompact.1 (hf hsy) with ⟨K, hKc, hKs⟩
  have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
  rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
  exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inr.ht
α : 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:
· exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Goal state after: