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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ u ^ ↑z = u ^ z

Tactic:
by
  change ((z : R) • Additive.ofMul u).toMul = _
  rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: case property
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*]

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯) ⟨i m, ⋯⟩ = ↑hnonempty.some.toLinearPMap ⟨i m, ⋯⟩

Tactic:
generalize_proofs _ _ h1

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
pf✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) '' c)
pf✝ : i m ∈ (LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) pf✝¹).domain
h1 : i m ∈ hnonempty.some.domain
⊢ ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) pf✝¹) ⟨i m, pf✝⟩ = ↑hnonempty.some.toLinearPMap ⟨i m, h1⟩
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)
a : ↥(extensionOfMax i f).domain
r : R
eq1 : ↑x = ↑a + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap a + (extendIdealTo i f h y) r

Tactic:
obtain ⟨a, ha⟩ := a

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 : ↑x = ↑⟨a, ha⟩ + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m : ℕ
inst✝ : CharZero K
hnm : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hnm : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
simp [*]

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

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a))))

Tactic:
map_map

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x ↦ p x) ∘ fun x ↦ x % a) (Ico n (n + a)))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
by
  let e : { m | m < n ∧ n.Coprime m } ≃ {x ∈ range n | n.Coprime x} :=
    { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using! m.property⟩
      left_inv := fun m => by simp only [Subtype.coe_eta]
      right_inv := fun m => by simp only }
  rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]

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

Goal state before:
pp: case a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False

Tactic:
totient_one,

Goal state after:
case a
hp : 0 < 1
h : 1 = 1 - 1
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Tactic:
rintro rfl
      rw [totient_one, tsub_self] at h
      exact one_ne_zero h

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 + toIcoDiv hp a b • p = b

Tactic:
toIcoMod_add_toIcoDiv_zsmul

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

Tactic:
by
  apply toIcoDiv_eq_of_sub_zsmul_mem_Ico
  rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_right_comm]
  exact sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : p
⊢ IsOpen[inst✝] {_x | p}

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : ¬p
⊢ IsOpen[inst✝] {_x | p}

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case insert
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_1
s : Set ι
f : ι → Set X
a✝² : ι
s✝ : Set ι
a✝¹ : a✝² ∉ s✝
hs✝ : s✝.Finite
a✝ : interior (⋂ i ∈ s✝, f i) = ⋂ i ∈ s✝, interior (f i)
⊢ interior (⋂ i ∈ insert a✝² s✝, f i) = ⋂ i ∈ insert a✝² s✝, interior (f i)

Tactic:
simp [*]

Goal state after:
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 : ℤ
⊢ toIcoDiv hp a (b + ↑m * p) = toIcoDiv hp a b + m

Tactic:
simpa using toIcoDiv_add_zsmul hp a b m

Goal state after:
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 : ℤ
⊢ toIcoMod hp (a - ↑m * p) b = toIcoMod hp a b - ↑m * p

Tactic:
by
  simpa using toIcoMod_sub_zsmul' hp a b m

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ s = ∅ → 𝓝ˢ s = ⊥

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case pos
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
h✝ : q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case neg
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
h✝ : ¬q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
simp [*]

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2

Tactic:
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

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 ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x

Tactic:
rw [← nhdsWithin_prod_eq]

Goal state after:
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 ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x
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 ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x

Tactic:
rw [← nhdsWithin_prod_eq]

Goal state after:
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 ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
exact (continuousWithinAt_iff_continuousAt_domRestrict f xs).mpr (h ⟨x, xs⟩)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = ⨅ i, comap (fun x ↦ x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
    iInf_principal_finite hI, ← iInf_inf_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
subst t

Goal state after:
α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ 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 : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map f (map (Prod.mk a) (𝓝 b))) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x ↦ f (a, x)) (𝓝 x)

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x ↦ f (a, x)) (𝓝 x)
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 : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map f (map (fun a ↦ (a, b)) (𝓝 a))) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun a ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ x1 ∩ x2) B₁ B₂)

Tactic:
refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
  rw [nhds_inf (t₁ := t₁)]
  convert! ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id
  aesop

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s (n + 1) ⊆ s k

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ a ∈ interior (I.pi s) ↔ a ∈ I.pi fun i ↦ interior (s i)

Tactic:
simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: 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

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: 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

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x | P a x} ∈ f

Tactic:
convert! f.finite_biUnion_mem_iff his (s := P) with i

Goal state after:
case e'_1
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} = ⋃ i ∈ is, P i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
p : ↑(countableBasis α) → α
hp : ∀ (s : ↑(countableBasis α)), p s ∈ ↑s
⊢ SeparableSpace α

Tactic:
exact ⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>
          ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i

Tactic:
apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
h : IsLocallyClosed (range f)
⊢ LocallyCompactSpace X

Tactic:
rcases h with ⟨U, Z, hU, hZ, hUZ⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
⊢ LocallyCompactSpace X
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst✝¹] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ ∀ a ⊆ s, a.Finite → (univ ∩ ⋂₀ a).Nonempty

Tactic:
by simpa using hs

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst✝¹] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ (⋂₀ s).Nonempty

Tactic:
by
  simpa using isCompact_univ.nonempty_inter_sInter hsc (by simpa using hs)

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

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

Tactic:
by simpa using hs

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

Goal state before:
pp: Y : Type v
inst✝ : TopologicalSpace Y
K : Set Y
X : Type u_2
l : Filter X
s : Set (X × Y)
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y
⊢ s ∈ ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
by simpa using hs

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l
⊢ s ∈ ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
by simpa using hs

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y
⊢ s ∈ ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
by simpa using hs

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg
α : 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 ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : x ∉ frontier {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:
rcases hx with hx | hx

Goal state after:
case neg.inl
α : 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

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
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y) = 𝓝 (mk x, mk y)

Tactic:
← prod_map_map_eq',

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ map mk (𝓝 x) ×ˢ map mk (𝓝 y) = 𝓝 (mk x, mk y)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ s_1 ⊆ s, ∃ u, IsOpen[inst✝] u ∧ s ∩ u = s_1) ↔ ∀ t ⊆ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = t

Tactic:
inter_comm

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
by
  constructor <;> intro H
  · exact fun i ↦ H.image <| continuous_apply i
  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1.h
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
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' u ∩ s

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2.h
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
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' v ∩ s

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ ∀ u_1 ∈ {U, u, v}, IsOpen[inst✝] u_1

Tactic:
simp [*]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Subsingleton
⊢ IsClosed[inst✝¹] s

Tactic:
rcases hs.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
  · exact isClosed_empty
  · exact isClosed_singleton

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ ∀ (i : Bool), IsDiscrete (bif i then s else t)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ ∀ (i : Bool), IsClosed[inst✝] (bif i then s else t)

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ

Tactic:
simp [*]

Goal state after: