mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : M
⊢ f m = ExtensionOfMaxAdjoin.extensionToFun i f h ⟨i m, ⋯⟩

Tactic:
(extensionOfMax i f).is_extension,

Goal state after:
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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ = ExtensionOfMaxAdjoin.extensionToFun i f h ⟨i m, ⋯⟩
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
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
obtain ⟨g', hg'⟩ := Module.Injective.out (eR.symm.toLinearMap ∘ₗ I.subtype ∘ₗ eI.toLinearMap)
    (eR.symm.injective.comp <| Subtype.val_injective.comp eI.injective) (g ∘ₗ eI.toLinearMap)

Goal state after:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ 𝓝 x ≤ f

Tactic:
rw [nhds_def]; exact iInf₂_le_of_le s ⟨h, o⟩ sf

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
rw [nhdsWithin, inf_neBot_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
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
s : Set X
⊢ ⇑h '' closure[inst✝¹] s = closure[inst✝] (⇑h '' s)

Tactic:
rw [← preimage_symm, preimage_closure]

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
⊢ Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb

Goal state after:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 (t ∩ t'ᶜ)

Tactic:
← inf_principal,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ (𝓟 t ⊓ 𝓟 t'ᶜ)
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
← inf_principal,

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ u ×ˢ ⋃ i ∈ t, i = Prod.fst ⁻¹' u

Tactic:
← sUnion_eq_biUnion,

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ u ×ˢ ⋃₀ t = Prod.fst ⁻¹' u
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ (⋃ i ∈ s, i) ×ˢ v = Prod.snd ⁻¹' v

Tactic:
← sUnion_eq_biUnion,

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃₀ s ×ˢ v = Prod.snd ⁻¹' v
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
ι' : Type u_9
φ : ι' → ι
⊢ induced (fun f j ↦ f (φ j)) topologicalSpace = ⨅ i', induced (eval (φ i')) (T (φ i'))

Tactic:
simp [Pi.topologicalSpace, induced_iInf, induced_compose, comp_def]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inl
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
j : ι
g : Y → A j
xi : A j
hg : Tendsto g l (𝓝 xi)
⊢ Tendsto (fun i ↦ Function.update (f i) j (g i) j) l (𝓝 (Function.update x j xi j))

Tactic:
simp [*, hf.apply_nhds]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
hj : j ≠ i
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
simp [*, hf.apply_nhds]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, generateFrom B] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)

Tactic:
continuous_generateFrom_iff

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ (∀ s ∈ B, IsOpen[t] (f ⁻¹' s)) ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
⊢ Disjoint (accumulate s i) (s j)

Tactic:
apply disjoint_left.2 (fun x hx ↦ ?_)
  simp only [accumulate, mem_iUnion, exists_prop] at hx
  rcases hx with ⟨k, hk, hx⟩
  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : 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
⊢ s ∩ f ⁻¹' t ⊆ w

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:
· exact (inter_comm _ _).trans_subset <| (inter_subset_inter_left _ <| preimage_mono hv.2.1).trans
      (hw.2.trans_subset inter_subset_left)

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.Compactness.Compact

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

pp: case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
· simp [sup_prod, *]

Goal state after:
case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∈ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
exact subset_union_right (subset_upperClosure hat)

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ⤳ y
hd : Disjoint (𝓝 x) (𝓝 y)
⊢ ¬Disjoint (𝓝 x) (𝓝 x)

Tactic:
by simp [NeBot.ne']

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

Goal state before:
pp: case htn
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := ⋯
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ∀ (i : { U // U ∈ c }), (↑i)ᶜ.Nonempty

Tactic:
exact fun U => (hc U.2).2.2

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, 𝓝 x ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)

Tactic:
ht.inf_nhdsSet_eq_biSup,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ 𝓝ˢ (s ∩ t)
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ y ∈ closure[inst✝¹] {x}

Tactic:
by_contra e

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : y ∉ closure[inst✝¹] {x}
⊢ False
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 Y
f : X → Y
s : Set X
c : Y
h : ∀ x ∈ closure[inst✝²] s, ContinuousWithinAt f s x
ht : EqOn f (fun x ↦ c) s
⊢ EqOn f (fun x ↦ c) (closure[inst✝²] s)

Tactic:
intro x hx
  apply ContinuousWithinAt.eq_const_of_mem_closure (h x hx) hx ht

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 ({x | x ⤳ p} ∩ s) ≤ 𝓝[s] p

Tactic:
← inf_principal,

Goal state after:
case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 {x | x ⤳ p} ⊓ 𝓟 s ≤ 𝓝[s] p
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
⊢ IsClosedEmbedding (update x i)

Tactic:
refine .of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
    (update_injective x i) fun s hs ↦ ?_
  rw [update_image]
  apply isClosed_set_pi
  simp [forall_update_iff, hs]

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

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
ext x
  simp only [boolIndicator, mem_preimage]
  split_ifs <;> simp [*]

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

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
this : (t ∩ (v ∩ u)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩

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

Goal state before:
pp: case refine_2.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (inl '' t)

pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)

Tactic:
· exact ht.image _ continuous_inl.continuousOn

Goal state after:
case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (inl '' t)

pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)

Tactic:
· exact ht.image _ continuous_inl.continuousOn

Goal state after:
case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
← inf_principal,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ⊓ 𝓟 t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
by
  constructor <;> intro h
  · intro u v hu hv hs huv
    specialize h u v hu hv hs
    contrapose! huv
    simp only [not_subset] at huv
    rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
    have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
    have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
    exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩
  · intro u v hu hv hs hsu hsv
    by_contra H
    specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)
    apply H
    rcases h with h | h
    · rcases hsv with ⟨x, hxs, hxv⟩
      exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
    · rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r : Set ι, r.Countable ∧ (t ⊆ ⋃ i ∈ r, U i) := by
    intro x hx
    let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
    refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
    simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
    exact Subset.refl _

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst✝¹] t ∧ t ⊆ s

Tactic:
by
  have h' := (regularSpace_TFAE X).out 0 3
  exact h'.mp ‹_› _ _ h

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t

Tactic:
rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
    exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst✝¹] U₁
U₂_op : IsOpen[inst✝¹] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst✝¹] V₁ ∧
            IsClosed[inst✝¹] V₂ ∧ IsOpen[inst✝¹] U₁ ∧ IsOpen[inst✝¹] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst✝¹] U₁
U₂_op : IsOpen[inst✝¹] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed[inst✝¹] V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst✝¹] V₁ ∧
            IsClosed[inst✝¹] V₂ ∧ IsOpen[inst✝¹] U₁ ∧ IsOpen[inst✝¹] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case h.left
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ (⋃ i_1 ∈ s, r i_1).Countable

Tactic:
refine (Countable.biUnion_iff hs).mpr ?h.left.a

Goal state after:
case h.left.a
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ a ∈ s, (r a).Countable
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ IsPreconnected s ↔ ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b

Tactic:
refine ⟨?_, fun H a b ha hb hsab hsa hsb ↦ ?_⟩

Goal state after:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
⊢ IsPreconnected s → ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b

case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ (s ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v

Tactic:
apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ⊆ u ∪ v

case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
t' : β
ht' : t' ∈ t
⊢ f ⁻¹' {t'} ∩ (u ∩ v) = ∅