mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = ZPow.toPow

Tactic:
by with_implicit rfl

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
Order.covBy_iff_add_one_eq,

Goal state after:
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a ⋖ b
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
· exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)

Goal state after:
case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = p ^ t * ((k + 2) / p ^ t)

Tactic:
Nat.mul_div_cancel' hpt

Goal state after:
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = k + 2
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case inr
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
exact multiplicative_factorization _ h_mult hf1 hn

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

Goal state before:
pp: n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
refine dvd_trans (Finset.prod_dvd_prod_of_dvd _ _ fun p hp ↦ ?_) this

Goal state after:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ p ^ (φ n / (p - 1)) ∣ p ^ φ n
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 c : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
by
  simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]

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 : α
⊢ b - toIocDiv hp a b • p ≤ b - (toIcoDiv hp a b • p - p)

Tactic:
sub_le_sub_iff_left,

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

Tactic:
simpa using toIocDiv_zsmul_add hp a b m

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ n a

Tactic:
intro U hU
    replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)
    refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩
    rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩
    exact (hopen x i hpi).mono fun y ↦ by gcongr

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen[TopologicalSpace.coinduced π inst✝] V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
by rwa [hf.isOpen_preimage]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure[inst✝¹] s
⊢ ContinuousWithinAt f s x

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x
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:
Prod.map_def,

Goal state after:
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 (fun p ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_2
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
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g

Tactic:
rw [(isOpenQuotientMap_snd (X := X)).isOpenMap_iff]

Goal state after:
case refine_2
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
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap (g ∘ Prod.snd)
Module: Mathlib.Topology.Bases

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

Tactic:
by
  refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩
  rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
  exact isOpen_iUnion fun s => hf s s.2.1

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis (fun t ↦ t ∈ preimage f '' T ∧ a ∈ t) id

Tactic:
convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
s : Set α
⊢ s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ (preimage f ∘ fun t ↦ t) '' {i | i ∈ T ∧ f a ∈ i}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen[t] u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, ↑a ∈ v ∧ v ⊆ u

Tactic:
rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩

Goal state after:
case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen[t] u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
v : Set ↑(U i)
hvb : v ∈ b i
hav : a ∈ v
hvu : v ⊆ Subtype.val ⁻¹' u
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, ↑a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t ∈ B, ∃ u, IsOpen[t✝] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst✝] t
⊢ ∃ u, IsOpen[t✝] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
obtain ⟨ι, g, rfl, hg⟩ := hB.open_eq_iUnion ht

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst✝] (⋃ i, g i)
⊢ ∃ u, IsOpen[t] u ∧ (f ⁻¹' ⋃ i, g i) ∩ s = u ∩ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
rw [← continuousOn_univ, ← hs']

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ ContinuousOn f (⋃ i, s i)
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
refine le_antisymm ?_ ?_
  · apply le_generateFrom
    rintro _ ⟨s, i, hi, rfl⟩
    let := fun a => generateFrom (g a)
    exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))
  · classical
    refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
    simp [hs]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
g : Filter α
hg : g.NeBot
hgu : g ≤ Filter.comap m ↑u
⊢ Filter.comap m ↑u ≤ g

Tactic:
simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : 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'
u : Set α
hu : u ∈ s'
⊢ ∃ f, f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u

Tactic:
simpa [t', and_assoc] using s't' hu

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Goal state after:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
simp only [← nhdsWithin_univ] at hf
  rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩
  exact ⟨s, hsc, univ_subset_iff.1 hsU⟩

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Subtype.val '' γ
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
rcases ha with ⟨_, ha, rfl⟩

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst✝] sᶜ)

Tactic:
rintro ⟨t, ⟨htcl, htco⟩, hst⟩
    exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm.symm) s ↔ f.symm.symm.symm b ∈ s

Tactic:
← symm_map,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm.symm.symm b ∈ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
← univ_prod_univ

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case left
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
i : ι
⊢ IsCompact (Sigma.mk i ⁻¹' u)

pp: case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
⊢ ((↑s).sigma fun i ↦ Sigma.mk i ⁻¹' u) = u

Tactic:
· exact Topology.IsClosedEmbedding.sigmaMk.isCompact_preimage hu

Goal state after:
case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
⊢ ((↑s).sigma fun i ↦ Sigma.mk i ⁻¹' u) = u
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝²] S
hne : S.Nonempty
V : Set X
Vsub : V ⊆ S
Vne : V.Nonempty
Vcls : IsClosed[inst✝²] V
hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst✝²] V' → V' = V
⊢ ∃ x ∈ S, IsClosed[inst✝²] {x}

Tactic:
rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝²] S
hne : S.Nonempty
x : X
Vsub : {x} ⊆ S
Vne : {x}.Nonempty
Vcls : IsClosed[inst✝²] {x}
hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed[inst✝²] V' → V' = {x}
⊢ ∃ x ∈ S, IsClosed[inst✝²] {x}
Module: Mathlib.Topology.Irreducible

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

Tactic:
rw [← mem_preimage] at hxu hyv

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

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

Tactic:
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
simp only [mem_codiscreteWithin, disjoint_principal_right]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
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
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)

Tactic:
hs.nhdsSet_inf_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 ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (f '' u)

Tactic:
suffices t ≤ closure (f '' f ⁻¹' t) from this.trans (closure_mono (image_mono htu))

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (f '' f ⁻¹' t)
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
intro z hz

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
z : X
hz : z ∈ t
⊢ ∃ t_1 ∈ 𝓝[≠] z, t_1 ∩ (t \ s) = ∅
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ ∀ z ∈ s, ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅

Tactic:
intro z hz

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ s = ⋃ i ∈ ∅, (fun x ↦ ∅) i

Tactic:
simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC

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

Goal state before:
pp: case insert
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ insert x t, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ insert x t, U i
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i

Tactic:
simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

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

Goal state before:
pp: case tail
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

Tactic:
| @tail j k _ hjk ih =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝²] (f ⁻¹' connectedComponentIn F y)

Tactic:
hf.continuous.continuousOn.preimage_connectedComponentIn

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝²] (⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x)