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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + c₁ + -c₂) = f x

Tactic:
h2.neg,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + c₁) = f x
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n

Tactic:
by_contra h : m ≠ n

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False
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)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, map_smul,
          LinearPMap.map_smul, ← smul_add]

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)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a)) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p ^ (n + 1) * a)

Tactic:
| succ n ih =>

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 : α
⊢ (∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b

Tactic:
exact fun ⟨i, hi⟩ =>
      ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
        ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ¬IsOpen {x} → Dense {x}ᶜ

Tactic:
· refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_
    obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
    exact ho hU

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✝ c : α
n : ℤ
a : α
b : α ⧸ AddSubgroup.zmultiples p
⊢ (fun x ↦ ↑↑x) ((fun b ↦ ⟨⋯.lift b, ⋯⟩) b) = b

Tactic:
induction b using QuotientAddGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ (fun x ↦ ↑↑x) ((fun b ↦ ⟨⋯.lift b, ⋯⟩) ↑z✝) = ↑z✝
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
toIocMod_eq_sub _ x₁,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp 0 (x₃ - x₁) + x₁ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ closure[inst✝] s ↔ 𝓝[s] x = ⊥

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ {x} ⊆ closure[inst✝] i'

Tactic:
singleton_subset_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ x ∈ closure[inst✝] i'
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen[inst✝] i ∧ s ⊆ i) ∧ i ⊆ t

Tactic:
by simp [mem_nhdsSet_iff_exists, and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Ico (a + n • p) (a + (n + 1) • p) = univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_
  rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩
  refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩
  rw [add_smul, one_smul, ← add_assoc]
  convert! sub_lt_iff_lt_add.mp hr using 1; abel

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
g : Set (Set α)
a : α
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
let := generateFrom g

Goal state after:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : 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 : α
⊢ 𝓝 a = n a

Tactic:
by
  let t : TopologicalSpace α := .mkOfNhds n
  apply le_antisymm
  · 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
  · exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t

Tactic:
rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩
    have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
    have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
        (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
        (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
        fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
      rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion,
        exists_false, not_false_eq_true]
    refine
      ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
       ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
       open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
       open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
       cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
       cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
       ?_⟩
    rw [Set.disjoint_left]
    rintro x ⟨un, ⟨n, rfl⟩, xinun⟩
    suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
    intro m xinvm
    have n_le_m : n ≤ m := by
      by_contra m_gt_n
      exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
    exact subset_closure (mem_biUnion n_le_m xinun.1)

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:
by simp [dense_iff_closure_eq]

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
haveI := ta1; haveI := tb1; exact Continuous fun p : X × Y => f p.1 p.2

Goal state after:
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 : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x ↦ f (g x, h x)) x

Tactic:
by
  rw [← e] at hf
  exact hf.comp₂ hg hh

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst✝] t
u : Set α
u_open : IsOpen[inst✝¹] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen[inst✝¹] (f ⁻¹' t ∩ s)

Tactic:
hu

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst✝] t
u : Set α
u_open : IsOpen[inst✝¹] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen[inst✝¹] (u ∩ s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case mp
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) → U ∈ pure x ⊔ cofinite

pp: case mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t

Tactic:
· rintro ⟨V, hVU, V_op, haV⟩
    exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩

Goal state after:
case mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
s : Set (CofiniteTopology X)
⊢ s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite

Tactic:
simp [nhds_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
huo : IsOpen[instTopologicalSpaceSubtype] u
hud : Dense u
⊢ ∃ v, IsOpen[inst✝] v ∧ Dense v ∧ Subtype.val ⁻¹' v = u

Tactic:
choose v hv1 hv2 using huo

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
hud : Dense u
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ ∃ v, IsOpen[inst✝] v ∧ Dense v ∧ Subtype.val ⁻¹' v = u
Module: Mathlib.Topology.Constructions.SumProd

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

Tactic:
rw [← disjoint_principal_left]
    exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
simp only [continuousOn_iff_continuous_domRestrict, (h.restrictPreimage_isOpen hs).continuous_iff]
  rfl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
⊢ IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
hu

Goal state after:
case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
⊢ ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
suffices ⋃ x ∈ s, interior (f x) = univ from
    ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ⋃ x ∈ s, interior (f x) = univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
⊢ ∃ w ∈ s u, x ∈ w

Tactic:
by simpa using this

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
⊢ u ∈ s' → (f u).Countable

Tactic:
hu

Goal state after:
case refine_1
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ (f u).Countable
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
⊢ u ∈ s' → f u ⊆ {s | IsOpen[ts] s}

Tactic:
hu

Goal state after:
case refine_2.a
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ f u ⊆ {s | IsOpen[ts] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
⊢ u ∈ s' → u ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}

Tactic:
hu

Goal state after:
case a
α : 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'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ u ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
by
  let b :=
    (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
  have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
  have B : b.Countable :=
    (Countable.image (countable_countableBasis _) _).union
      (Countable.image (countable_countableBasis _) _)
  exact A.secondCountableTopology B

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ n, compactCovering X n = univ

Tactic:
rw [compactCovering, iUnion_accumulate]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ x, ⋯.choose x = univ
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
⊢ Nonempty (CompactExhaustion X)

Tactic:
let K : ℕ → { s : Set X // IsCompact s } := fun n =>
    Nat.recOn n ⟨∅, isCompact_empty⟩ fun n s =>
      ⟨(exists_compact_superset s.2).choose ∪ compactCovering X n,
        (exists_compact_superset s.2).choose_spec.1.union (isCompact_compactCovering _ _)⟩

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K✝ : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
K : ℕ → { s // IsCompact s } := fun n ↦ Nat.recOn n ⟨∅, ⋯⟩ fun n s ↦ ⟨⋯.choose ∪ compactCovering X n, ⋯⟩
⊢ Nonempty (CompactExhaustion X)
Module: Mathlib.Order.UpperLower.Closure

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

Tactic:
simp [f.le_symm_apply]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
Filter.mem_cocompact

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Prod.fst ⁻¹' K.1ᶜ ∪ univ ×ˢ K.2ᶜ ∈ cocompact (X × Y)

Tactic:
← prod_univ,

Goal state after:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ K.1ᶜ ×ˢ univ ∪ univ ×ˢ K.2ᶜ ∈ cocompact (X × Y)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)

Tactic:
simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map,
    continuousWithinAt_lift₂]
  rfl

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
⊢ IsOpen[inst✝] u → IsOpen[inst✝] v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hu

Goal state after:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen[inst✝] u
⊢ IsOpen[inst✝] v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
by_cases h₁x : x ∈ U

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ IsOpen[inst✝²] U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
rw [isOpen_iff_ultrafilter]
  refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
  intro cond x hx f h
  rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
  exact cond _ hx

Goal state after: