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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCountableCoproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
⊢ ∀ [inst : Countable J], HasExactColimitsOfShape (Discrete J) C

Tactic:
by_cases h : Finite J
    · infer_instance
    · have : Infinite J := ⟨h⟩
      let _ := Encodable.ofCountable J
      let _ := Denumerable.ofEncodableOfInfinite J
      exact hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ s.π.app (L.obj j) ≫ α.app j = { pt := s.1, π := L.whiskerLeft s.π ≫ α }.π.app j

Tactic:
NatTrans.comp_app,

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ s.π.app (L.obj j) ≫ α.app j = (L.whiskerLeft s.π).app j ≫ α.app j
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
inst✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)

Tactic:
by
  rw [← essentiallySmall_congr
    (StructuredArrow.pre S (equivSmallModel.{w} C).inverse T).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsDetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsDetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op X
⊢ ∃! h', h' ≫ f.op = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCodetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCodetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : P.op G
h : op Y ⟶ G
⊢ ∃! h', f.op ≫ h' = h
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case snd
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)

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

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

Tactic:
dsimp [negOnePow]

Goal state after:
n : ℤ
⊢ (-1) ^ (-n) = (-1) ^ n
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:
| cons g l ih =>

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

Goal state before:
pp: a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
⊢ motive (k + 2)

Tactic:
haveI hp : Prime p := minFac_prime (succ_succ_ne_one k)

Goal state after:
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
⊢ motive (k + 2)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
intro b

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
⊢ b < d * x → (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
m : ℕ
hn : 0 < m.succ
⊢ φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)

Tactic:
exact totient_prime_pow_succ hp _

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

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2

Tactic:
intro b

Goal state after:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ ∃ a, b ⊆ a.1 ×ˢ a.2
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ ∃ a, b ⊆ a.1 ×ˢ a.2

Tactic:
use (Finset.image Prod.fst b, Finset.image Prod.snd b)

Goal state after:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ⊆ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)

Tactic:
simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]

Goal state after:
case mp
m n : ℕ
⊢ 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u_2
t₁ t₂ : TopologicalSpace X
⊢ t₁ = t₂ ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s

Tactic:
by
  rw [TopologicalSpace.ext_iff, compl_surjective.forall]
  simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
by rw [Function.comp_apply, hg', principal_univ]

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 + c) = toIocMod hp (a - c) b + c

Tactic:
by
  simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]
  refine iInf_congr ?_
  rintro (_ | _) <;> rfl

Goal state after:
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:
simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi

Goal state after:
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:
simp_rw [interior_eq_nhds, subset_def, mem_ofPred]

Goal state after:
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
s'₁ : Set Y
hs₁ : IsOpen[t] s'₁
s'₂ : Set Y
hs₂ : IsOpen[t] s'₂
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = f ⁻¹' s'₁ ∩ f ⁻¹' s'₂

Tactic:
exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩

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 : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
_root_.add_comm (toIocMod _ _ _),

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - c) + toIocMod hp 0 (b - a)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp a (↑m * p + b) = toIcoMod hp a b

Tactic:
simpa using toIcoMod_zsmul_add hp a b m

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

Goal state before:
pp: 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
⊢ TopologicalSpace.coinduced p inst✝² = TopologicalSpace.induced g inst✝

Tactic:
by
  ext U
  change IsOpen (p ⁻¹' U) ↔ ∃ V, _
  simp_rw [hf.isOpen_iff,
    (Set.image_surjective.mpr hq.surjective).exists,
    ← hq.isQuotientMap.isOpen_preimage]
  constructor
  · rintro ⟨V, hV, e⟩
    refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩
    ext x
    obtain ⟨x, rfl⟩ := hp x
    constructor
    · rintro ⟨y, hy, e'⟩
      obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
      rw [← hg ((congr_fun h y).trans e')]
      exact e.le hy
    · intro H
      exact ⟨f x, e.ge H, congr_fun h.symm x⟩
  · rintro ⟨V, hV, rfl⟩
    refine ⟨_, hV, ?_⟩
    simp_rw [← Set.preimage_comp, h]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: 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)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
⊢ {x | U ∈ n x} ∈ n x

Tactic:
rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩

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)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
i : ι x
hpi : p x i
hi : s x i ⊆ U
⊢ {x | U ∈ n x} ∈ n x
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
obtain ⟨u, u_cov, u_props⟩ := sc_st
  exact
    ⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst✝] s ⊆ closure[inst✝¹] (f ⁻¹' s)

Tactic:
← compl_subset_compl

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ (closure[inst✝¹] (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure[inst✝] s)ᶜ
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst✝¹] K
⊢ IsClosed[inst✝] (g '' K)

Tactic:
rw [← image_preimage_eq K hf, ← image_comp]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst✝¹] K
⊢ IsClosed[inst✝] (g ∘ f '' f ⁻¹' K)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
by
  simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
by
  lift a to t using h
  replace hs : (fun x : t => X x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
  rwa [← map_nhds_subtype_val, mem_map]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
by rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ IsTopologicalBasis s

Tactic:
convert! isTopologicalBasis_of_subbasis hsg

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ s = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]

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

Goal state before:
pp: 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)

Tactic:
have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id :=
      h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin

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
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ

Tactic:
IsClosedEmbedding.inr.closure_image_eq,

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ Sum.inr '' closure[inst✝²] t = univ
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f

Tactic:
exact hp (of_le f) (H _ ((of_le f).trans hfg))

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)

Tactic:
rw [Filter.frequently_smallSets' hq, hl.forall_iff hq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : 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'
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u :=
    fun u hu ↦ by simpa [t', and_assoc] using s't' hu

Goal state after:
α : 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'
A : ∀ u ∈ s', ∃ f, f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

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

Goal state before:
pp: α : Type u_2
A : Set α
D E : Set ↑A
⊢ D ⊆ A ↓∩ Subtype.val '' E ↔ D ⊆ E

Tactic:
preimage_image_eq _ Subtype.val_injective

Goal state after:
α : Type u_2
A : Set α
D E : Set ↑A
⊢ D ⊆ E ↔ D ⊆ E
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]
  tauto

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty

Tactic:
refine h _ ?_ fun Q hQP hQ ↦ ?_

Goal state after:
case refine_1
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
⊢ compl '' P ⊆ 𝔅

case refine_2
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ (⋂₀ Q).Nonempty
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
⊢ IsCompact t

Tactic:
intro f _ hf
  obtain ⟨x, hxs, hxf⟩ := hs <| hf.trans <| Filter.monotone_principal hts
  obtain ⟨y, hyt, hxy⟩ := h x hxs
  exact ⟨y, hyt, hxy.clusterPt hxf⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst✝] z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

Tactic:
refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, IsClosed[inst✝] z) →
      s ⊆ ⋃₀ ↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t) →
        ∃ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, s ⊆ z
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst✝] U
h : (S ∩ U).Nonempty
⊢ S ⊆ closure[inst✝] (S ∩ U)

Tactic:
by_contra h'

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst✝] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst✝] (S ∩ U)
⊢ False
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
⊢ V' = Uᶜ

Tactic:
have : V'ᶜ = U := by
    refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
    · exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)
    · simp only [compl_compl, V'ne]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = Uᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
⊢ (f ⁻¹' Z).Nonempty

Tactic:
by obtain ⟨x, hx⟩ := hV.1.1; exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩

Goal state after:
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]

Goal state after: