mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
Module: Mathlib.Algebra.Group.Nat.Range

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

Tactic:
by
  rw [← val_inj, union_val]
  exact Multiset.range_add_eq_union a b

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x

Tactic:
simp

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

Goal state before:
pp: case H
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ⋯⟩ + 0 • y

Tactic:
simp

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

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

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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = (RingHom.id R) r • ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩

Tactic:
by rw [← LinearPMap.map_smul]; dsimp

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

Goal state before:
pp: case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ f 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)

Tactic:
hf

Goal state after:
case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ (divisors 0).sum φ = 0

Tactic:
simp

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

Goal state before:
pp: case e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (0 + 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

Tactic:
simp

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

Goal state before:
pp: case e'_2.hab
n : ℕ
⊢ 0 < n.succ

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
X : Type u_3
s : ι → Set X
⊢ ⋃ i ∈ ∅, s i = ∅

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: ⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2

Tactic:
simp

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

Goal state before:
pp: ⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2

Tactic:
simp

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

Goal state before:
pp: ⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2

Tactic:
simp

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

Goal state before:
pp: case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0

Tactic:
simp

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

Goal state before:
pp: case inl
a : ℕ
ha : ¬a = 0
hb : ¬a * 1 = 0
this : a.Coprime 1
⊢ a = a * 1 ∨ 2 * a = a * 1

Tactic:
simp

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 : α
⊢ a = a + 0 • p

Tactic:
simp

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 : α
⊢ a = a + p + -1 • p

Tactic:
simp

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 : α
⊢ a + p = a + 1 • p

Tactic:
simp

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 : α
⊢ a + p = a + p + 0 • p

Tactic:
simp

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 : α
m : ℤ
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Tactic:
by
  rw [add_comm, toIocDiv_add_zsmul, add_comm]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case empty
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_1
s : Set ι
f : ι → Set X
⊢ interior (⋂ i ∈ ∅, f i) = ⋂ i ∈ ∅, interior (f i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = (closure sᶜ)ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝] i → ∃ x ∈ i, p x) ↔ ∀ (U : Set X), x ∈ U → IsOpen[inst✝] U → ∃ y ∈ U, p y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
intro U U_op x_in

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ x ∉ interior {x | x ∉ s}

Tactic:
closure_eq_compl_interior_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ (interior sᶜ)ᶜ ↔ x ∉ interior {x | x ∉ s}
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
simp

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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ = x₁ + p + -1 • p

Tactic:
simp

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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' = x₃' - p + 1 • p

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst✝]
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure[inst✝], s = t₁ ∩ t₂) → s.Nonempty
⊢ {x} ∈ pure x

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
⊢ toIcoMod hp a b - b = -↑(toIcoDiv hp a b) * p

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
⊢ toIocMod hp a b - b = -↑(toIocDiv hp a b) * p

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
⊢ b - toIcoMod hp a b = ↑(toIcoDiv hp a b) * p

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
⊢ b - toIocMod hp a b = ↑(toIocDiv hp a b) * p

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
⊢ toIocMod hp a b + ↑(toIocDiv hp a b) * p = b

Tactic:
simpa using toIocMod_add_toIocDiv_zsmul hp a b

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ 𝓝ˢ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inl.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ ∅ = ∅ ∨ ∅ ∩ ∅ = univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inl.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ ∅ ∩ univ = ∅ ∨ ∅ ∩ univ = univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inr.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ univ ∩ ∅ = ∅ ∨ univ ∩ ∅ = univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inr.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ univ = ∅ ∨ univ ∩ univ = univ

Tactic:
simp

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
⊢ range ⇑h = univ

Tactic:
simp

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
⊢ (∀ (x : Set Y), IsOpen[inst✝¹] (f ⁻¹' xᶜ) ↔ IsOpen[inst✝] xᶜ) ↔
    ∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
simp

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
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: case e'_2
X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst✝²] (⇑e ⁻¹' s) ↔ IsOpen[inst✝¹] s
s : Set X
⊢ s = ⇑e ⁻¹' ⇑e.symm ⁻¹' s

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ IsCoinducing g ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g

Tactic:
hf.surjective.of_comp_iff

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ IsCoinducing g ∧ Surjective g ↔ IsCoinducing g ∧ Surjective g
Module: Mathlib.Topology.Order

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

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
e : X ≃ Y
⊢ ∀ (s : Set Y), IsOpen[inst✝⁴] (⇑e ⁻¹' s) ↔ IsOpen[inst✝³] s

Tactic:
simp

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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ≤ 𝓟 {x}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst✝] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u] a

Tactic:
nhdsWithin_restrict u h₀ h₁,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst✝] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ⊆ L ∪ R

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ R ⊆ L ∪ R

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ ∅, s i] a = ⨆ i ∈ ∅, 𝓝[s i] a

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Tactic:
simp

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_5
⊢ univ.Nonempty → univᶜ.Finite

Tactic:
simp

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_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋃₀ s)ᶜ.Finite

Tactic:
rw [compl_sUnion]

Goal state after:
X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋂₀ (compl '' s)).Finite
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x ⊤
hh : AccPt x (𝓟 {x}ᶜ)
⊢ 𝓟 {x}ᶜ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
hsg : t✝ = generateFrom s
hsi : FiniteInter s
t : Set α
ht : t ∈ s
⊢ {t} ∈ {f | f.Finite ∧ f ⊆ s} ∧ (fun f ↦ ⋂₀ f) {t} = t

Tactic:
simpa using ht

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ ∅, ∀ t₂ ∈ ∅, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ∅, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ {∅}, ∀ t₂ ∈ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s

Tactic:
rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']

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:
simp

Goal state after:
α : 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 ⊆ s k ∧ s (n + 1) ⊆ s k
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case neg
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
· use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
α✝ : Type ?u.21
a : α✝
s : Set α✝
⊢ sᶜ ∉ pure a ↔ s ∈ pure a

Tactic:
simp

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

Goal state before:
pp: α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
⊢ f.NeBot → f ≤ g → p f

Tactic:
hf

Goal state after:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
⊢ f ≤ g → p f
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: case empty
α : Type u
f : Ultrafilter α
s : Set (Set α)
⊢ ⋃₀ ∅ ∈ f ↔ ∃ t ∈ ∅, t ∈ f

Tactic:
simp

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 : IsOpen[inst✝ i] s
⊢ ∀ (i_1 : ι), IsOpen[inst✝ i_1] (Sigma.mk i_1 ⁻¹' Sigma.mk i '' s)

Tactic:
intro j

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)
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
⊢ ∀ (i_1 : ι), IsClosed[inst✝ i_1] (Sigma.mk i_1 ⁻¹' Sigma.mk i '' s)

Tactic:
intro j

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

Goal state before:
pp: case neg
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t = ∅
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
exact ⟨fun n => ∅, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
by
  let B := { b ∈ countableBasis α | ∃ i, b ⊆ s i }
  choose f hf using fun b : B => b.2.2
  have : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype
  refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩
  rintro _ ⟨i, rfl⟩ x xs
  rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
  exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.h₁
α : 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 : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
x : α
hx : x ∈ u
⊢ x ∈ ⋃ i, a ↑i

Tactic:
simp

Goal state after:
case refine_2.h₁
α : 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 : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
x : α
hx : x ∈ u
⊢ ∃ i ∈ u, x ∈ a i
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.h₂
α : 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 : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ ⋃ i, a ↑i ⊆ u

Tactic:
simp

Goal state after:
case refine_2.h₂
α : 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 : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ ∀ i ∈ u, a i ⊆ u
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: case e'_2
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∀ t ∈ l, p t) ↔ ¬∃ s ∈ l, ¬p s

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a.h
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
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'
i : Set α
hi : i ∈ f u
⊢ i ∈ ⋃ u ∈ s', f u

Tactic:
simp

Goal state after:
case a.h
α : 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'
i : Set α
hi : i ∈ f u
⊢ ∃ i_1 ∈ s', i ∈ f i_1
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ f <$> s <*> t

Tactic:
simp

Goal state after: