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✝¹ : AddSemigroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

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)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑(fst i x) - a = r • y - snd i x • y
⊢ ↑(fst i x) - a = (r - snd i x) • y

Tactic:
← sub_smul

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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑(fst i x) - a = (r - snd i x) • y
⊢ ↑(fst i x) - a = (r - snd i x) • y
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k ↦ p (b + k)) a + count p b = count (fun k ↦ p (k + b)) a + count p b

Tactic:
add_comm b

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

Goal state before:
pp: case neg.refine_1
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ 1 < a

pp: case neg.refine_2
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ (p ^ n).Coprime a

Tactic:
· contrapose! hpa
      simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]

Goal state after:
case neg.refine_2
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ (p ^ n).Coprime a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf ↑(-1)

Tactic:
Units.coe_neg_one,

Goal state after:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False

Tactic:
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ #(range (p ^ (n + 1)) \ image (fun x ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)

Tactic:
card_sdiff_of_subset h2,

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ #(range (p ^ (n + 1))) - #(image (fun x ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Tactic:
by
  simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (b + p) = toIocDiv hp a b + 1

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

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] (⋃₀ ∅)

Tactic:
exact isOpen_sUnion fun a => False.elim

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 : α
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ interior (⋂ i, f i) = ⋂ i, interior (f i)

Tactic:
← sInter_range,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ interior (⋂₀ range f) = ⋂ i, interior (f i)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ closure (⋃ i, f i) = ⋃ i, closure (f i)

Tactic:
← sUnion_range,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ closure (⋃₀ range f) = ⋃ i, closure (f i)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
by
  rw [← not_iff_not]
  simp only [not_frequently, eventually_eventually_nhds]

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 : α
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Tactic:
rw [toIcoMod_eq_iff, and_iff_left]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • p
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, ←
    exists_and_left, and_assoc, and_comm, and_left_comm]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom s

Tactic:
refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)
  rintro t (rfl | h)
  · exact ht
  · exact isOpen_generateFrom_of_mem h

Goal state after:
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
⊢ IsOpen[inst✝] (⇑h.symm ⁻¹' s) ↔ IsOpen[inst✝¹] s

Tactic:
isOpen_preimage

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen[inst✝¹] s ↔ IsOpen[inst✝¹] s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a

Tactic:
by
  rw [nhds_induced, Filter.map_comap, nhdsWithin]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
⊢ Continuous[inst✝, instTopologicalSpaceProd] fun y ↦ (x, y)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ Continuous[inst✝¹, instTopologicalSpaceProd] fun x ↦ (x, y)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a

Tactic:
← sUnion_range,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃₀ range s] a = ⨆ i, 𝓝[s i] a
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

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

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ Dense t ↔ s ⊆ closure[inst✝] ↑t

Tactic:
IsInducing.subtypeVal.dense_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : { x // x ∈ s }), ↑x ∈ closure[inst✝] (val '' t)) ↔ s ⊆ closure[inst✝] ↑t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim inl (inr ∘ inl))

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[inst✝, instTopologicalSpaceSum] (inr ∘ inr)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[inst✝², instTopologicalSpaceSum] (inl ∘ inl)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim (inl ∘ inr) inr)

Tactic:
fun_prop

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 : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ ContinuousOn (fun b ↦ (a, b)) sβ

Tactic:
fun_prop

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 : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ ContinuousOn (fun a ↦ (a, b)) sα

Tactic:
fun_prop

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

Goal state before:
pp: 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
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
simp_rw [isEmbedding_iff, isInducing_sumElim, Sum.elim_injective]
  constructor
  · intro ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, f_ne_g⟩⟩
    exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
  · intro ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
    refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
    exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ ∀ (x : α) (o : Set β), IsOpen[inst✝¹] o → f x ∈ o → (o ∩ f '' invFun f '' s).Nonempty

Tactic:
intro x U hU hx

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst✝¹] U
hx : f x ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ i, s i) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
← sUnion_range,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃₀ range s) ↔ ∀ (i : ι), IsBounded (s i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' closure[t✝] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ

Tactic:
hsd.closure_eq,

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] {x}

Tactic:
by
    rw [← univ_pi_singleton]
    exact isOpen_set_pi finite_univ fun i _ => (isOpen_discrete {x i})

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
obtain ⟨g, hg⟩ := Filter.exists_seq_tendsto (𝓝 x ⊓ f)

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
g : ℕ → α
hg : Tendsto g atTop (𝓝 x ⊓ f)
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ f ∘ ULift.down)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(ULift.{v, u} X, ULift.{u, v} Y)
⊢ Continuous[inst✝¹, inst✝] (ULift.down ∘ ⇑f ∘ ULift.up)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ ⇑f ∘ ULift.down)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i ∩ U] a = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, f i ∩ U] a

Tactic:
simp only [mem_ofPred_eq, iUnion_nonempty_self]

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Finite

Tactic:
simpa only [hne] using! hf.finite_nonempty_of_compact

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsSigmaCompact s
hf : ContinuousOn f s
⊢ IsSigmaCompact (f '' s)

Tactic:
rcases hs with ⟨K, hcompact, hcov⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ IsSigmaCompact (f '' s)
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]
  exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

Goal state after:
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
K : ℕ → { s // IsCompact s } := fun n ↦ Nat.recOn n ⟨∅, ⋯⟩ fun n s ↦ ⟨⋯.choose ∪ compactCovering X n, ⋯⟩
⊢ Nonempty (CompactExhaustion X)

Tactic:
refine ⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩

Goal state after:
case refine_1
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, ⋯⟩
n : ℕ
⊢ ↑(K n) ⊆ interior ↑(K (n + 1))

case refine_2
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, ⋯⟩
⊢ ⋃ n, ↑(K n) = univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : s ∩ ⋂ i, t i = ∅
hdt : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
⊢ s ⊆ ⋃ i, (compl ∘ t) i

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop,
          mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using! hst

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l f : Filter X
⊢ f ⊓ l = comap Function.diag (f ×ˢ l)

Tactic:
simpa only [comap_prod] using! congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
⊢ IsBounded (f '' s)

Tactic:
by
  choose U hU using hf
  obtain ⟨I, hI⟩ := hs.elim_nhds_subcover U (fun x _ => (hU x).1)
  have : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x := by simp [Set.image_iUnion₂]
  exact ((isBounded_biUnion_finset I).2 fun i _ => (hU i).2).subset (this ▸ Set.image_mono hI.2)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.ht
α : 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}ᶜ) x

Tactic:
· have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Goal state after:
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
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact univ

Tactic:
rw [Sigma.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
X : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (⋃ a, range (Sigma.mk a))
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : X
s : Set X
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y

Tactic:
lift y to s using hys

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : IrreducibleSpace ↑s
⊢ IsIrreducible s

Tactic:
exact ⟨.of_subtype, .of_subtype⟩

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
· rw [h.symm.nhdsWithin_compl_singleton] at hb
    exact hb.filter_mono nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
⊢ Z ⊆ f '' V

Tactic:
have := hV.2 ⟨(by obtain ⟨x, hx⟩ := hV.1.1; exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩),
      hZ.2.preimage_of_isPreirreducible_fiber f hf₂ hf₃⟩ (Set.image_subset_iff.mp hWZ)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
this : f ⁻¹' Z ⊆ V
⊢ Z ⊆ f '' V
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
z : X
H : ContinuousWithinAt f s z
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z

Tactic:
exact H.mono sdiff_subset

Goal state after: