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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j

Tactic:
have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
      F'.hom_ext_of_isRightKanExtension α _ _ (by cat_disch)
    exact congr_app this

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h

Tactic:
· obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)
    rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
by
  simpa only [zsmul_eq_mul] using h.add_zsmul_eq n

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

Goal state before:
pp: 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
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
⊢ motive (p ^ n * a)

Tactic:
by_cases ha1 : a = 1

Goal state after:
case pos
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
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)

case neg
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
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ motive (p ^ n * a)
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)
hab_pos : a * b ≠ 0
⊢ ((a.factorization.prod fun p k ↦ f (p ^ k)) * b.factorization.prod fun p k ↦ f (p ^ k)) =
    (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
factorization_mul_of_coprime hab,

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
⊢ ((a.factorization.prod fun p k ↦ f (p ^ k)) * b.factorization.prod fun p k ↦ f (p ^ k)) =
    (a.factorization + b.factorization).prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
by
  rw [← pow_one p, totient_prime_pow hp] <;> simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
by
  rw [← Filter.eventually_forall_le_atBot] at h_evtl; exact (h_evtl.comap f).filter_mono hf.le_comap

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
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p

Tactic:
convert! toIcoMod_mem_Ico hp 0 b

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ p = 0 + p
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 : α
⊢ toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_sub_zsmul hp a b 1

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 α
⊢ t₁ ∈ f.sets → ∀ y ∈ f.sets, ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) y z

Tactic:
ht₁

Goal state after:
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
⊢ ∀ y ∈ f.sets, ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) y z
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsOpen[inst✝] s) fun x ↦ x

Tactic:
convert! nhds_basis_opens x using 2
  exact and_congr_left_iff.2 IsOpen.mem_nhds_iff

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 x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
simp_rw [Set.mem_ofPred, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
    not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_forall_notMem_Ioo_mod hp, not_forall,
    Classical.not_not]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S

Tactic:
rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ⋃ y ∈ S, f ⁻¹' g y = ⋃ i ∈ S, i
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ -toIcoDiv hp a z✝ • p ∈ AddSubgroup.zmultiples p

Tactic:
apply AddSubgroup.zsmul_mem_zmultiples

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ -toIocDiv hp a z✝ • p ∈ AddSubgroup.zmultiples p

Tactic:
apply AddSubgroup.zsmul_mem_zmultiples

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

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

Tactic:
by
  simpa using toIocDiv_add_zsmul hp a b m

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
f : Filter X
s : Set X
⊢ 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Tactic:
by simp [nhdsSet]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝ˢ {x} = 𝓝 x

Tactic:
by simp [nhdsSet]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b

Tactic:
rwa [update_of_ne hb]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_2
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ U = ∅ ∨ U = univ → IsOpen[⊤] U

Tactic:
rintro (rfl | rfl)
    exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
nontrivialTopology_iff

Goal state after:
α : Type u
t : TopologicalSpace α
⊢ t ≠ ⊤ ↔ t ≠ ⊤
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
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
simp_rw [Filter.le_def, mem_comap'', ← subset_interior_iff_mem_nhdsSet,
    ← subset_kernImage_iff, isClosedMap_iff_kernImage_interior]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[{a}] a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a

Tactic:
nhdsWithin_singleton

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ pure a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))

Tactic:
simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]

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

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[instTopologicalSpaceSum] Z
⊢ IsClosed[inst✝] (f '' Z)

Tactic:
rw [isClosed_sum_iff] at hZ

Goal state after:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
⊢ IsClosed[inst✝] (f '' Z)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ

Tactic:
rw [sUnion_image, iUnion₂_eq_univ_iff]
    exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
⊢ ContinuousOn g s₁

Tactic:
by
  intro x hx
  unfold ContinuousWithinAt
  have A := (h x (h₁ hx)).mono h₁
  unfold ContinuousWithinAt at A
  rw [← h' hx] at A
  exact A.congr' h'.eventuallyEq_nhdsWithin.symm

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi
  push _ ∈ _ at hy
  exact not_imp_not.mp (hy i) hi

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
rcases K.exists_mem x with ⟨n, hn⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : x ∈ K n
⊢ ∃ n, K n ∈ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
by
  simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]
  tauto

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
⊢ ↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)

Tactic:
simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact (range f)

Tactic:
exact isCompact_range hf

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hf
α : 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})
⊢ ContinuousOn f (s ∩ {a | p a})

Tactic:
exact hf.mono (inter_subset_inter_right s subset_closure)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ U ∈ codiscreteWithin U

Tactic:
simp [mem_codiscreteWithin]

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

Goal state before:
pp: case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' s)

Tactic:
rw [← compl_compl s, preimage_compl]

Goal state after:
case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' sᶜ)ᶜ
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure[inst✝¹] K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
  contrapose! hy
  have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
  simpa only [disjoint_iff, notMem_closure_iff_nhdsWithin_eq_bot]
    using! this.mono_right principal_le_nhdsSet

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

Tactic:
by
  refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩ <;> intro H u v hu hv hss huv
  · apply H u v hu hv hss
    rw [huv.inter_eq, inter_empty]
  have H1 := H (u ∩ s) (v ∩ s)
  rw [subset_inter_iff, subset_inter_iff] at H1
  simp only [Subset.refl, and_true] at H1
  apply H1 (hu.inter hs) (hv.inter hs)
  · rw [← union_inter_distrib_right]
    exact subset_inter hss Subset.rfl
  · rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅

Tactic:
by
  refine eq_empty_iff_forall_notMem.2 fun x hx => ?_
  rw [mem_interior_iff_mem_nhds] at hx
  have := di.closure_image_mem_nhds hx
  rw [(hs.image di.continuous).isClosed.closure_eq] at this
  rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
  exact hyi (image_subset_range _ _ hys)

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
⊢ LocallyConnectedSpace X

Tactic:
have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s)
      (h.symm '' ·) := fun x ↦ by
    rw [← h.symm_map_nhds_eq]
    exact (i.1 _).map _
  refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
  exact hs.2.2.2.image _ h.symm.continuous.continuousOn

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

Goal state before:
pp: α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
c : α
hc : c ∈ Prod.mk b ⁻¹' V
⊢ c ∈ Prod.mk a ⁻¹' id U

Tactic:
exact hVU ⟨b, hb, hc⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
let cl_d := { p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.map f f) atTop

Tactic:
rw [mem_map, mem_atTop_sets]

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ a, ∀ (b : β × β), a ≤ b → b ∈ Prod.map f f ⁻¹' s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous id

Tactic:
rw [uniformContinuous_iff_le_comap, uniformSpace_comap_id, id]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩
  rcases hf r hr with ⟨k, fk, ks⟩
  let u := k ∩ { y | ∃ x ∈ s, (x, y) ∈ r }
  choose g hgs hgr using fun x : u => x.coe_prop.2
  refine ⟨range g, ?_, ?_, ?_⟩
  · exact range_subset_iff.2 hgs
  · have : Fintype u := (fk.inter_of_left _).fintype
    exact finite_range g
  · filter_upwards [hs, ks] with x xs ⟨y, hy, xy⟩
    simp_rw [SetRel.preimage, exists_range_iff]
    set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩
    exact ⟨z, rU ⟨y, xy, rs (hgr z)⟩⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ f ≤ 𝓟 (m '' s), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ≤ 𝓟 s, Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
← mem_Iic (b := 𝓟 _),

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ f ∈ Iic (𝓟 (m '' s)), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y

Tactic:
by
  rcases lebesgue_number_lemma (U := fun x => interior (U x)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
  exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

Goal state after: