mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case mpr
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₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  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 α

Tactic:
apply Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
      (E := Functor.LeftExtension.mk _ α)

Goal state after:
case mpr
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₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  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
⊢ (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
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
f g : Subobject.underlying.obj ⊥ ⟶ A
⊢ IsSplitEpi (equalizer.ι f g)

Tactic:
exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
      ext
      simp⟩

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

Goal state after:
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)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_2
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} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inl ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      f

Tactic:
intro T

Goal state after:
case mpr.refine_2
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
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    (c.inl ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      f
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
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} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inr ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      g

Tactic:
intro T

Goal state after:
case mpr.refine_3
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
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    (c.inr ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      g
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ -f (x + ↑n * (2 * c)) = -f x

Tactic:
h.int_even_mul_periodic

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ -f x = -f x
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop

Tactic:
by
  cases isEmpty_or_nonempty α
  · subsingleton
  cases isEmpty_or_nonempty β
  · subsingleton
  simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

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

Goal state before:
pp: p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
refine ⟨fun h => ?_, totient_prime⟩

Goal state after:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Tactic:
rintro rfl

Goal state after:
case a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 1 * (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
apply Nat.mul_lt_mul_of_le_of_lt

Goal state after:
case inr.hac
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 1 ≤ (c ^ 2)!

case inr.hbd
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

case inr.hc
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 0 < (c ^ 2)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p ∈ n.primeFactors, ↑p ≠ 0

Tactic:
← cast_prod,

Goal state after:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(∏ i ∈ n.primeFactors, i) ≠ 0
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Tactic:
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]

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

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

Tactic:
simpa [(totient_pos.2 hp.pos).ne', mul_comm] using h1

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 : α
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1

Tactic:
rw [add_comm, toIocDiv_add_right]

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

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₂ z

Tactic:
exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩

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

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

Tactic:
rw [add_comm, toIcoMod_add_zsmul', add_comm]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a (a + z • p) = a + p

Tactic:
rw [toIocMod_add_zsmul, toIocMod_apply_left]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = (⋃₀ {t | IsOpen t ∧ t ⊆ sᶜ})ᶜ

Tactic:
compl_sUnion,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ (compl '' {t | IsOpen t ∧ t ⊆ sᶜ})
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s ∩ (closure s ∩ (interior s)ᶜ) = ∅

Tactic:
← inter_assoc,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s ∩ closure s ∩ (interior s)ᶜ = ∅
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (interior s)ᶜ ∩ (interior s ∩ closure s) = ∅

Tactic:
← inter_assoc,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (interior s)ᶜ ∩ interior s ∩ closure s = ∅
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s

Tactic:
rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ frontier univ = ∅

Tactic:
by simp [frontier]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ frontier ∅ = ∅

Tactic:
by simp [frontier]

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
by
  rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ ClusterPt x (Filter.map u F) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i

Tactic:
hx.clusterPt_iff_frequently,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ (∀ (i : ι), p i → ∃ᶠ (x : X) in Filter.map u F, x ∈ s i) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
insert_eq,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ ({x} ∪ s) = 𝓝 x ⊔ 𝓝ˢ s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
apply forall_congr' (fun x ↦ ?_)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
⊢ {x} ∈ 𝓝 x ↔ 𝓝 x = pure x
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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (𝓝 (f x)) ≤ 𝓝 (g (f x))

Tactic:
← hf.map_nhds_of_mem _ h,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (map f (𝓝 x)) ≤ 𝓝 (g (f x))
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓝 a ⊓ 𝓟 (s ∩ t)

Tactic:
inf_idem

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 (s ∩ t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[inst✝¹] (f ⁻¹' Subtype.val '' x✝)

Tactic:
(hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[inst✝¹] (Subtype.val '' s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[inst✝¹] (f ⁻¹' Subtype.val '' x✝)
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s ≠ ∅

Tactic:
rintro rfl

Goal state after:
α : Type u_2
x✝ : Bornology α
h : ¬IsBounded ∅
⊢ False
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u

Tactic:
← inter_assoc,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ w ∩ s ∩ f ⁻¹' t' ⊆ f ⁻¹' u
Module: Mathlib.Topology.Bases

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

Tactic:
← hf u hu,

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ⋂₀ f u ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
refine hf.surjective.forall.2 fun x U hU ↦ ?_

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
⊢ (do
      let a ← γ
      pure ↑a) ⊆
    β

Tactic:
intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert! ha

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

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

Tactic:
image_sUnion,

Goal state after:
α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ ⋃₀ (image Subtype.val '' T) = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
change sᶜ ∈ Filter.cocompact X ↔ _

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen[inst✝³] {x}

Tactic:
obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst✝²] U
hU₃ : f x ∈ U
⊢ IsOpen[inst✝³] {x}
Module: Mathlib.Topology.Clopen

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a ∩ (b ∩ s) = ∅

Tactic:
← inter_assoc,

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a ∩ b ∩ s = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
replace huv := subset_inter huv Subset.rfl

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ s ∩ (u' ∩ (s ∩ v'))
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
← inter_assoc,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ s ∩ u' ∩ (s ∩ v')
⊢ (f '' s ∩ (u ∩ v)).Nonempty