mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft (e.hom ≫ e.inv) = α

Tactic:
e.hom_inv_id,

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft (𝟙 F') = α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f))

Tactic:
let φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) :=
      CostructuredArrow.homMk f

Goal state after:
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
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) := CostructuredArrow.homMk f ⋯
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
⊢ (fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ })
      ((fun f ↦
          { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
            naturality := ⋯ })
        f) =
    f

Tactic:
ext X
    let e : CostructuredArrow.mk
      (uliftYonedaEquiv.{max w v₂}.symm (X.hom.app (op X.left) ⟨𝟙 X.left⟩)) ≅ X :=
        CostructuredArrow.isoMk (Iso.refl _) (by
          ext Y x
          dsimp
          simp [← NatTrans.naturality_apply])
    simpa [e] using! f.naturality e.inv

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)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g

Tactic:
cases g

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map (line a✝)
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)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ F.map g ≫ eqToHom ⋯ ≫ t.ι.app j' =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g

Tactic:
cases g

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
a✝ : J
⊢ F.map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
⊢ Subobject.underlying.obj ⊥ ⟶ A

Tactic:
let s : ∏ᶜ (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
      Pi.lift (fun f ↦ Pi.π Subtype.val ⟨f.right.obj, f.right.property⟩)

Goal state after:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
s : ∏ᶜ Subtype.val ⟶ ∏ᶜ P.productToFamily A := Pi.lift fun f ↦ Pi.π Subtype.val ⟨f.right.obj, ⋯⟩
⊢ Subobject.underlying.obj ⊥ ⟶ A
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑↑-[n+1].negOnePow = (-1) ^ -[n+1].natAbs

Tactic:
| negSucc n =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : CommMonoid β
ι : Type u_4
f : ι → α → β
s : Finset ι
hs : ∀ i ∈ s, Periodic (f i) c
⊢ ∀ f_1 ∈ List.map f s.toList, Periodic f_1 c

Tactic:
by simpa [-Periodic]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x

Tactic:
rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]

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)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = a + r • y
⊢ ↑(fst i x) - a = (r - snd i x) • y

Tactic:
rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1

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

Goal state before:
pp: case neg.refine_1
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
hpa : a ≤ 1
⊢ p ∣ a

Tactic:
simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n

Tactic:
rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Goal state after:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a n : ℕ
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = φ a

Tactic:
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]

Goal state after:
case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a
Module: Mathlib.Data.Nat.Totient

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

Tactic:
simp_rw [← totient_eq_one_iff]

Goal state after:
case mpr
m n : ℕ
⊢ φ m = 1 ∨ φ n = 1 → (φ m).Coprime (φ n)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
rintro (h | h)

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)

case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
by
  rsuffices ⟨φ, hφ, hrφ⟩ : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
  · exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩
  have : ∀ t : Set ℕ, t.Finite → ∀ᶠ n in atTop, ∀ m ∈ t, m < n ∧ r m n := fun t ht =>
    (eventually_all_finite ht).2 fun m _ => (eventually_gt_atTop m).and (hr _)
  rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩
  simp only [forall_mem_image, forall_and, mem_Iio] at hφ
  exact ⟨φ, forall_comm.2 hφ.1, forall_comm.2 hφ.2⟩

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
⊢ ∃ x, Tendsto x atTop f

Tactic:
choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)

Goal state after:
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
toIocMod_add_toIocDiv_zsmul

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

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : C(X, Y)
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h : { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toFun✝¹ : X → Y
continuous_toFun✝¹ : Continuous[inst✝¹, inst✝] toFun✝¹
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h :
  { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }
Module: Mathlib.Topology.Continuous

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

Tactic:
exact hg.dense_image cg hf

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

Goal state after:
case mpr.inl
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

case mpr.inr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)
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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]

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 : IsOpenEmbedding f
s : Set X
h : IsOpen[inst✝] (f '' s)
⊢ f ⁻¹' f '' s = s

Tactic:
apply preimage_image_eq _ hf.injective

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
hxy

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u

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

Goal state after:
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : c.Countable
hs : s ⊆ closure[t] c
⊢ IsSeparable u
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x✝ : X
hx : x✝ ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x✝
x : X
h₁ : x ∈ {x | x ∈ s → x ∈ t}
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False

Tactic:
exact h₂ (h₁ hs)

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

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K✝ : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
K : ℕ → { s // IsCompact s } := fun n ↦ Nat.recOn n ⟨∅, ⋯⟩ fun n s ↦ ⟨⋯.choose ∪ compactCovering X n, ⋯⟩
⊢ ⋃ n, compactCovering X n ⊆ ⋃ n, ↑(K n)

Tactic:
exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ×ˢ t)

Tactic:
by
  rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢
  intro f hfs
  obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
    hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)
  obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
    ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)
  rw [map_le_iff_le_comap] at hx hy
  refine ⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩
  rw [nhds_prod_eq]; exact le_inf hx hy

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
rw [sdiff_eq, inter_comm, nhdsWithin_inter_of_mem]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ {y}ᶜ ∈ 𝓝[s] x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
← eventually_nhdsSet_iff_forall,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ᶠ (x : X × X) in 𝓝ˢ (s ×ˢ s), f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t
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
this : f ⁻¹' Z ⊆ V
⊢ Z ⊆ f '' V

Tactic:
← Set.image_preimage_eq Z hf₄

Goal state after:
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
this : f ⁻¹' Z ⊆ V
⊢ f '' f ⁻¹' Z ⊆ f '' V
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
⊢ z ∈ U → ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
h₁z

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
z : X
H : ContinuousWithinAt (update f x y) s z
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z

Tactic:
continuousWithinAt_update_of_ne hz.2

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
z : X
H : ContinuousWithinAt f s z
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
⊢ z ∈ U → ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
h₁z

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Module: Mathlib.Topology.Order.LeftRight

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

Tactic:
simp only [← Ici_sdiff_left, continuousWithinAt_sdiff_self]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_insert, insert_sdiff_singleton, continuousWithinAt_insert]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
t : OrderClosedTopology α
⊢ IsClosed[instTopologicalSpaceProd] (diagonal α)

Tactic:
by
    simpa only [diagonal, le_antisymm_iff] using!
      t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)

Tactic:
rcases H with ⟨x, hx⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
⊢ False

Tactic:
obtain ⟨x, -, hxU, hxV⟩ := hs U V (isOpen_biUnion fun i a ↦ hs' i)
    (isOpen_biUnion fun i a ↦ hs' i) hsplit.le hUne hVne

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
hxU : x ∈ U
hxV : x ∈ V
⊢ False
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
by
  refine ⟨fun S hSc hS => ?_⟩
  choose s hs t ht hst using hS
  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
  refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
  rw [hst i hi]
  apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)

Goal state after: