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✝³ : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5OfSize.{w₂, w₂', v, u} C
⊢ AB5OfSize.{w, w', v, u} C

Tactic:
by
  have : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
  constructor
  intro J _ _
  have := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
  exact HasExactColimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
A : C
x✝ : P A
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op A)).map f))

Tactic:
exact (h A).2

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
A : C
x✝ : P A
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj A).map f.op))

Tactic:
exact (h A).2

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso f → ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))) → IsIso f

Tactic:
· intro h
    rw [isIso_iff_coyoneda_map_bijective] at h
    intro A _
    exact (h A).2

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))) → IsIso f
Module: Mathlib.CategoryTheory.Subobject.Comma

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✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫
      S.map (Subobject.underlyingIso (MonoOver.mk f).arrow.unop.left.op).unop.inv ≫ (unop P).hom =
    A.hom

Tactic:
by
      dsimp
      rw [← Category.assoc, ← S.map_comp, ← unop_comp]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ ∀ (Y : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements)
    (m : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X)) ⟶ Y),
    m = ⟨shrinkYonedaObjObjEquiv Y.snd, ⋯⟩

Tactic:
by
    rintro u ⟨m, hm⟩
    ext
    simp [← hm, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ ↑n * (q / ↑n) = q

Tactic:
(Int.cast_commute n _).eq,

Goal state after:
𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ q / ↑n * ↑n = q
Module: Mathlib.Algebra.Ring.NegOnePow

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

Tactic:
simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ {x | btw a x b}ᶜ ↔ ¬btw a x✝ b

Tactic:
mem_compl_iff,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ ¬x✝ ∈ {x | btw a x b} ↔ ¬btw a x✝ b
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ ¬sbtw a x✝ b

Tactic:
cIoo,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ {x | sbtw a x b}ᶜ ↔ ¬sbtw a x✝ b
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ {x | sbtw a x b}ᶜ ↔ ¬sbtw a x✝ b

Tactic:
mem_compl_iff,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ ¬x✝ ∈ {x | sbtw a x b} ↔ ¬sbtw a x✝ b
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
  · rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

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

Tactic:
mul_div_cancel_right₀ _ hn

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑k = ↑k
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
cast_div hm,

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑m / ↑d / ↑(n / d) = ↑m / ↑n

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
⊢ a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
hab_pos

Goal state after:
case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

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

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

Tactic:
· rw [← not_imp_not]
    simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
    exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2

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

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

Tactic:
by
  rw [multiplicative_factorization φ (@totient_mul) totient_one hn]
  apply Finsupp.prod_congr _
  intro p hp
  have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
  rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]

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

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

Tactic:
simp [ha, h']

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
Nat.totient_prime_pow hp hk,

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ (p ^ (k - 1) * (p - 1)) / ∏ x ∈ (p ^ k).primeFactors, x ^ (p ^ (k - 1) * (p - 1) / (x - 1)) =
    p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
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 (p + a) b = toIocDiv hp a b - 1

Tactic:
rw [add_comm, toIocDiv_add_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 : α
⊢ toIocDiv hp (a - p) b = toIocDiv hp a b + 1

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

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

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
y : Set β₁
⊢ ((f₂.lift g₂).lift' fun t ↦ y ×ˢ t) = f₂.lift fun s ↦ (g₂ s).lift' fun t ↦ y ×ˢ t

Tactic:
apply lift'_lift_assoc hg₂

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ (interior sᶜ)ᶜ ↔ x ∉ interior {x | x ∉ s}

Tactic:
mem_compl_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ interior sᶜ ↔ x ∉ interior {x | x ∉ s}
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ ∅
⊢ interior (frontier s) = ∅

Tactic:
subset_empty_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) = ∅
⊢ interior (frontier s) = ∅
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ x ∉ (interior s)ᶜ

Tactic:
mem_compl_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ¬x ∉ interior s
Module: Mathlib.Topology.ClusterPt

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

Tactic:
U

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
U : Set X
⊢ U ∈ F.lift' closure[inst✝] → U ∈ pure x
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ

Tactic:
Set.inter_comm

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen[t] xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
by simp only [preimage_compl, compl_inj_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤

Tactic:
nontrivialTopology_iff,

Goal state after:
α : Type u
t : TopologicalSpace α
⊢ instTopologicalSpace α t ≠ ⊤ ↔ t ≠ ⊤
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst✝] s ↔ x ∈ closure[induced f inst✝¹] s

Tactic:
hf.eq_induced

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[induced f inst✝¹] s ↔ x ∈ closure[induced f inst✝¹] s
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ map (⇑h.symm) (𝓝 (h x)) = 𝓝 x

Tactic:
rw [h.symm.map_nhds_eq, h.symm_apply_apply]

Goal state after:
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
x : X
f : Y → Z
⊢ inst✝¹ = induced (fun x_1 ↦ x) inst✝² ⊓ induced (fun x ↦ f x) inst✝ ↔ inst✝¹ = induced f inst✝

Tactic:
induced_const,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ inst✝¹ = ⊤ ⊓ induced (fun x ↦ f x) inst✝ ↔ inst✝¹ = induced f inst✝
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
y : Y
f : X → Z
⊢ inst✝² = induced (fun x ↦ f x) inst✝ ⊓ induced (fun x ↦ y) inst✝¹ ↔ inst✝² = induced f inst✝

Tactic:
induced_const,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ inst✝² = induced (fun x ↦ f x) inst✝ ⊓ ⊤ ↔ inst✝² = induced f inst✝
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)

Tactic:
← disjoint_principal_right

Goal state after:
case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ Disjoint (𝓝 (f x)) (𝓟 (range g))
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 : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x ↦ f (x, b)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_comm (α := α) (β := β), nhds_prod_eq,
    nhds_discrete, prod_pure, map_map]; rfl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
⊢ ∀ (o : Set β), IsOpen[inst✝¹] o → f x ∈ o → (o ∩ f '' invFun f '' s).Nonempty

Tactic:
U

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
⊢ IsOpen[inst✝¹] U → f x ∈ U → (U ∩ f '' invFun f '' s).Nonempty
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ((fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i) ∧
    a i ∈ (fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i

Tactic:
simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]

Goal state after:
case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ⋯.choose ∧ a i ∈ ⋯.choose
Module: Mathlib.Topology.Bases

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

Tactic:
· choose! U' hU' hUU' using hUT
    exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
by
    rw [nhds_pi, Filter.mem_pi] at hn
    obtain ⟨s, hs, n', hn', hsub⟩ := hn
    choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
    refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
    · exact (set_pi_mem_nhds_iff hs _).mpr fun i _ => hn'' i
    · exact forall₂_imp fun i _ hi' => hsub' i hi'
    · classical
      rw [← Set.univ_pi_ite]
      refine isCompact_univ_pi fun i => ?_
      by_cases h : i ∈ s
      · rw [if_pos h]
        exact hc i
      · rw [if_neg h]
        exact CompactSpace.isCompact_univ

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
⊢ ∀ (u : Set Y), y ∈ u → IsOpen[inst✝] u → ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ u

Tactic:
U

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
⊢ y ∈ U → IsOpen[inst✝] U → ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
⊢ U '' s ⊆ S

Tactic:
by simpa [Set.subset_def]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedCompact X).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) compl

Tactic:
simp only [Filter.coclosedCompact, iInf_and']

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed[inst✝] s ∧ IsCompact s), 𝓟 sᶜ).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) compl
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : n ∈ 𝓝ˢ s ×ˢ 𝓝ˢ t
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : ∃ i, ((IsOpen[inst✝¹] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst✝] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg
α : 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 ∈ s
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x

Tactic:
rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
    rcases hx with hx | hx
    · apply ContinuousWithinAt.union
      · exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
      · 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
    · apply ContinuousWithinAt.union
      · have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
      · exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ closure[inst✝²] {a | p a}] a) (𝓝 (f a))

Tactic:
exact hf a ⟨ha.1, ha.2.1⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ∀ s_1 ∈ (fun x ↦ closure[inst✝] {x}) '' s, IsClosed[inst✝] s_1

Tactic:
rintro _ ⟨_, _, rfl⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w✝ : X
left✝ : w✝ ∈ s
⊢ IsClosed[inst✝] ((fun x ↦ closure[inst✝] {x}) w✝)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z

Tactic:
apply Set.Subset.antisymm

Goal state after:
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

Tactic:
intro h x hx y hy
    by_contra e
    obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := r1_separation fun h => e h.specializes.mem_closure
    exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a

Tactic:
by
  rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]

Goal state after: