mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE f ⋯ = s.fst

pp: case refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯ = s.snd

pp: case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯

Tactic:
· cat_disch

Goal state after:
case refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯ = s.snd

case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case e_7
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
inst✝ : L.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ (CostructuredArrow.map (𝟙 Y)).obj j = j

Tactic:
apply CostructuredArrow.map_id

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'
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
e : L.LeftExtension F
⊢ StructuredArrow.IsUniversal e ≃ StructuredArrow.IsUniversal ((precomp L F G).obj e)

Tactic:
apply IsInitial.isInitialIffObj (LeftExtension.precomp L F G)

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

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)

Tactic:
exact kernel.lift _ _ (cokernel.condition f)

Goal state after:
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, w, max v₂ w} (StructuredArrow S ((equivSmallModel C).inverse ⋙ T))

Tactic:
exact essentiallySmall_of_small_of_locallySmall _

Goal state after:
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 : C ⥤ D
T : D
inst✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w} (CostructuredArrow ((equivSmallModel C).inverse ⋙ S) T)

Tactic:
exact essentiallySmall_of_small_of_locallySmall _

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 ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ L.IsLeftKanExtension e.hom

Tactic:
by
  rw [isLeftKanExtension_along_uliftYoneda_iff]
  exact ⟨inferInstance, ⟨inferInstance⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily J
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id.line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, Hom.id zero ≫ line a✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, zero, Hom.id zero with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case line.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, line a✝ ≫ Hom.id one with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match one, one, Hom.id one with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
· cat_disch

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

Goal state before:
pp: case mpr.refine_1
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ {T : Type u} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

Tactic:
intro T f g
        refine ↾fun x => ?_
        exact
          if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
          else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ count p n ≤ #hp.toFinset

Tactic:
rw [count_eq_card_filter_range]
  exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ #(range (p ^ (n + 1))) - #(range (p ^ n)) = p ^ n * (p - 1)

Tactic:
card_range,

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ (n + 1) - #(range (p ^ n)) = p ^ n * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ (n + 1) - #(range (p ^ n)) = p ^ n * (p - 1)

Tactic:
card_range,

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ (n + 1) - p ^ n = p ^ n * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ n * N (b % n) ≤ b

Tactic:
exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
rw [hb, totient_zero, totient_eq_zero] at h'
    exact False.elim (ha h')

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))

Tactic:
mul_left_comm

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed[inst✝] (f i)
⊢ IsClosed[inst✝] (⋃ i ∈ s, f i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Goal state after:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen[inst✝] (f i)ᶜ
⊢ IsOpen[inst✝] (⋂ i ∈ s, (f i)ᶜ)
Module: Mathlib.Topology.Basic

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

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Goal state after:
X : Type u
ι : Sort v
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (s i)ᶜ
⊢ IsOpen[inst✝¹] (⋂ i, (s i)ᶜ)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)

Tactic:
· rintro (h | h)
    · exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩
    · exact h.clusterPt

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ (F.lift' closure[inst✝] ⊓ pure x).NeBot

Tactic:
rw [clusterPt_iff_lift'_closure, inf_comm]
  constructor
  · intro h
    simp [h, pure_neBot]
  · intro h U hU
    simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
    simpa using h ({x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

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 : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
⊢ btw x₁ x₂ x₃ ∨ btw x₃ x₂ x₁

Tactic:
by
      induction x₁ using QuotientAddGroup.induction_on
      induction x₂ using QuotientAddGroup.induction_on
      induction x₃ using QuotientAddGroup.induction_on
      simp_rw [btw_coe_iff]
      apply toIxxMod_total

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

Goal state before:
pp: case mpr
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
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V

Tactic:
simp_rw [← Set.preimage_comp, h]

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ Disjoint (⋃ n, u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) (⋃ n, v n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), u m))

Tactic:
Set.disjoint_left

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ ∀ ⦃a : X⦄,
    a ∈ ⋃ n, u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m) → a ∉ ⋃ n, v n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), u m)
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s ∩ vᶜ ∪ t ∩ vᶜ

Tactic:
(disjoint_compl_right.mono_left htv).inter_eq,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s ∩ vᶜ ∪ ∅
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ sᶜ = (s ∪ t)ᶜ ∪ v

Tactic:
rw [← compl_inj_iff, Set.compl_union, compl_compl, compl_compl, union_inter_distrib_right,
    (disjoint_compl_right.mono_left htv).inter_eq, union_empty, left_eq_inter, subset_compl_comm]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ v ⊆ sᶜ
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x ↦ X ↑x) ⁻¹' s ∈ 𝓝 a
⊢ X ⁻¹' s ∈ 𝓝[t] ↑a

Tactic:
rwa [← map_nhds_subtype_val, mem_map]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Tactic:
refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
⊢ s ∈ 𝓝 x.1
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ (x_1 : x ∈ s), ⟨x, ⋯⟩ ∈ J) ↔ ∃ (x_1 : x ∈ t) (h : x ∈ s), ⟨x, ⋯⟩ ∈ J

Tactic:
exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s₁ : Set X
s₂ : Set Y
h₁ : IsClosed[inst✝¹] s₁
h₂ : IsClosed[inst✝] s₂
⊢ closure[instTopologicalSpaceProd] (s₁ ×ˢ s₂) = s₁ ×ˢ s₂

Tactic:
simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ t₁ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
    ∀ t₂ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
      ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h

Goal state after:
case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : t₁.Finite
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : t₂.Finite
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f ↦ ⋂₀ f) t₁ ∩ (fun f ↦ ⋂₀ f) t₂
⊢ ∃ t₃ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ (fun f ↦ ⋂₀ f) t₁ ∩ (fun f ↦ ⋂₀ f) t₂
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (g ⁻¹' C) univ

Tactic:
← elim_comp_inr f g,

Goal state after:
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (Sum.elim f g ∘ inr ⁻¹' C) univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis ∅
⊢ IsEmpty α

Tactic:
simpa using h.sUnion_eq.symm

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)

Tactic:
simpa using (hf.continuousOn (s := univ)).preimage_mem_nhdsSetWithin h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst✝] f
⊢ IsSeparable (f '' s)

Tactic:
rcases hs with ⟨c, c_count, hc⟩

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ IsSeparable (f '' s)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Tactic:
simp_rw [← Subtype.exists_set_subtype, biUnion_image]

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ x ∈ ⋃ a ∈ s u, a

Tactic:
convert! xu

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ ⋃ a ∈ s u, a = u
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
Module: Mathlib.Topology.Compactness.SigmaCompact

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

Tactic:
rw [image_preimage_inter, inter_eq_left.mpr]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝ˢ {y}

Tactic:
exact hs.le_nhdsSet_of_clusterPt hmem h

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 1 → 2 := (pure_le_nhds _).trans

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.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:
have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

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

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

Tactic:
replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)

Goal state after:
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 ⊆ 𝔅
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty
⊢ (⋂₀ Q).Nonempty