mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
by
  constructor
  · intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction
  · exact negOnePow_odd n

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]

Goal state after:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
by
  simpa only [inv_inv] using h.const_smul a⁻¹

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
by
  simpa only [inv_inv] using h.const_smul a⁻¹

Goal state after:
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)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : b ∈ R ∙ y
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rw [Submodule.mem_span_singleton] at b_mem

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)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : ∃ a, a • y = b
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
← val_inj,

Goal state after:
a b : ℕ
⊢ (range (a + b)).val = (range a ∪ map (addLeftEmbedding a) (range b)).val
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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y

Tactic:
smul_eq_mul,

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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r * ExtensionOfMaxAdjoin.snd i a) • y
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop atTop

Tactic:
by
  rw [← prod_atTop_atTop_eq]
  exact tendsto_id.prodMk tendsto_id

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

Goal state before:
pp: a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
⊢ 0 < n → a * c ^ n < (n - d)!

Tactic:
hn0

Goal state after:
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ φ a ∣ φ b

Tactic:
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]

Goal state after:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ ⊥.lift' closure = ⊥

Tactic:
by rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
hs : Dense s
⊢ range f ⊆ closure[inst✝] (f '' s)

Tactic:
rw [← image_univ, ← hs.closure_eq]
  exact image_closure_subset_closure_image hf

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
s : Set α
⊢ Dense s ↔ s = univ

Tactic:
simp [dense_iff_closure_eq]

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 : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in 𝓝 x₀, p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x

Tactic:
rw [← eventually_nhdsSet_iff_forall] at H
  replace H := H.filter_mono hf.comap_nhds_le
  rwa [eventually_comap] at H

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 : IsOpenEmbedding f
x : X
l : Filter Y
⊢ AccPt x (comap f l) ↔ AccPt (f x) l

Tactic:
by
  rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ Tendsto f (𝓝[≠] a) (𝓝 (f a))

Tactic:
simp [ContinuousAt, -pure_sup_nhdsNE, ← pure_sup_nhdsNE a, tendsto_pure_nhds]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen[generateFrom s] ((fun f ↦ ⋂₀ f) t)

Tactic:
exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Goal state after:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
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 : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
by
  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]; rfl

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
S : Set ι
⊢ induced S.domRestrict topologicalSpace = ⨅ i ∈ S, induced (eval i) (T i)

Tactic:
by
  simp +unfoldPartialApp [← iInf_subtype'', ← induced_precomp' ((↑) : S → ι),
    domRestrict]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : 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 α
hu : u ∈ ⋃ i, image Subtype.val '' b i
⊢ IsOpen[t] u

Tactic:
simp only [mem_iUnion, mem_image] at hu

Goal state after:
case refine_1
α : 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 α
hu : ∃ i, ∃ x ∈ b i, Subtype.val '' x = u
⊢ IsOpen[t] u
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ

Tactic:
by
  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩
  contrapose!
  intro h n
  obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n
  grind

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

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

Tactic:
by
  rw [nonempty_iff_ne_empty]
  rintro rfl
  exact h isBounded_empty

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
⊢ (↑i).piecewise t c a ∈ g a

Tactic:
by_cases a ∈ i

Goal state after:
case pos
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∈ i
⊢ (↑i).piecewise t c a ∈ g a

case neg
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∉ i
⊢ (↑i).piecewise t c a ∈ g a
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)

Tactic:
by simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
rw [← biUnion_of_singleton s] at h'
  rcases (Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
  exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
⊢ IsClosed[instTopologicalSpaceSigma] (Sigma.mk i '' s)

Tactic:
rw [isClosed_sigma_iff]

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
⊢ ∀ (i_1 : ι), IsClosed[inst✝ i_1] (Sigma.mk i_1 ⁻¹' Sigma.mk i '' s)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ x, Function.uncurry K x)

Tactic:
exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)

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

Goal state before:
pp: case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ ⋃ n, (fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n = univ

Tactic:
· simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
      intro k y
      rcases exists_mem_compactCovering y with ⟨n, hn⟩
      refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
      exact compactCovering_subset _ (le_max_right _ _) hn

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
⊢ ∃ i, V i ⊆ W

Tactic:
by_contra! H

Goal state after:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), ¬V i ⊆ W
⊢ False
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
⊢ upperClosure t ⊓ s.sdiff t = s

Tactic:
rw [inf_comm, sdiff_inf_upperClosure hts hst]

Goal state after:
Module: Mathlib.Topology.Piecewise

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

Tactic:
· 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.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst✝] u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ a ∈ t, s ⊆ aᶜ

Tactic:
refine forall_congr' fun _ => Iff.trans ?_ not_imp_not

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
x✝ : ∀ u ∈ t, IsOpen[inst✝] u
⊢ (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ ↑t, aᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = Uᶜ

Tactic:
← this,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = V'ᶜᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U

Tactic:
rw [preirreducibleSpace_iff, isPreirreducible_iff_subset_closure_inter_open]
  simp only [univ_inter, univ_subset_iff, Dense]
  grind

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun x y ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Tactic:
simp only [t2Space_iff_disjoint_nhds, Filter.disjoint_iff, Pairwise]

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Disjoint Uf Ug
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
Set.disjoint_iff_inter_eq_empty

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Uf ∩ Ug = ∅
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Tactic:
continuousAt_iff_continuous_left_right

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a ↔
    ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
this : Finite ↑I
hs : ∀ (x : { a // a ∈ I }), IsDiscrete (s ↑x)
hsc : ∀ (x : { a // a ∈ I }), IsClosed[inst✝] (s ↑x)
⊢ IsDiscrete (⋃ x, s ↑x)

Tactic:
exact .iUnion hs hsc

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
hs : DiscreteTopology ↑S
ht : DiscreteTopology ↑T
hs' : IsClosed[inst✝] S
ht' : IsClosed[inst✝] T
⊢ DiscreteTopology ↑(S ∪ T)

Tactic:
by
  rw [← isDiscrete_iff_discreteTopology] at *
  exact hs.union ht hs' ht'

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE h]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Tactic:
rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ {b | f b ≤ g b} ∩ closure[inst✝] {b | f b ≤ g b}ᶜ ⊆ {b | f b = g b}
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α

Tactic:
by
  refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
  · rw [mem_ofPred_eq, compl_sInter]
    apply hUnion (compl '' S) (hSc.image _)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht
  · rw [mem_ofPred_eq]
    rw [← compl_subset_compl] at hsub
    exact hmono sᶜ ht tᶜ hsub

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩
  simp_rw [connectedComponentIn_eq_image hx] at h ⊢
  obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h
  simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]

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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
nth_rw 1 [this]

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : u = ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩
⊢ ⋃ i, ⋃ (x : i ∈ v), ⋃ (_ : i ∈ u), Subtype.val '' connectedComponent ⟨i, ⋯⟩ = ⋃ x ∈ u, connectedComponentIn v x
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case mp.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ f' '' t, b i ⊆ ⋃ i, (b ∘ f') i

Tactic:
apply Set.iUnion₂_subset
      rintro i hi
      obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi
      exact Set.subset_iUnion (b ∘ f') j

Goal state after: