mathlib-initiative/mathlib-tactics huggingface dataset:
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
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ (idealTo i f y) ⟨r, this⟩ = 0

Tactic:
dsimp [ExtensionOfMaxAdjoin.idealTo]

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
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨r • y, ⋯⟩ = 0
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
by
  rcases eq_or_ne d 0 with (rfl | hd); · simp [Nat.zero_dvd.1 hm]
  replace hd : (d : K) ≠ 0 := by norm_cast
  rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd] <;> exact hd

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

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

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simpa
  · exact multiplicative_factorization _ h_mult hf1 hn

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

Goal state before:
pp: case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0

Goal state after:
case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * 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 : α
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel_left, neg_smul]

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

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -toIcoDiv hp a (-b) = toIocDiv hp (-(a + p)) b
Module: Mathlib.Topology.Closure

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

Tactic:
by
  rw [interior, closure, compl_sUnion, compl_image_ofPred]
  simp only [compl_subset_compl, isOpen_compl_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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)

Tactic:
have h' := toIcoMod_mem_Ico hp a b

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
h' : toIcoMod hp a b ∈ Set.Ico a (a + p)
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ClusterPt x ⊤

Tactic:
by simp [ClusterPt]

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:
by
  rw [toIcoMod_eq_iff, and_iff_left]
  exact ⟨0, by simp⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
h : ∀ t_1 ∈ S, ∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
choose! g hgo hfg using h

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S
Module: Mathlib.Topology.Continuous

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

Tactic:
← image_univ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
hs : Dense s
⊢ f '' univ ⊆ closure[inst✝] (f '' s)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))

Tactic:
accPt_iff_clusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
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:
by
  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 t : Set X
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst✝] s) t

Tactic:
by
  rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
⊢ Continuous[t₂, t₃] f

Tactic:
continuous_iff_le_induced

Goal state after:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃
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
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝] (g ∘ f '' s)

Tactic:
image_comp

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
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝] (g '' f '' s)
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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst✝²] s
⊢ IsClosed[inst✝] (g ∘ f '' s)

Tactic:
image_comp

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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst✝²] s
⊢ IsClosed[inst✝] (g '' f '' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})

Tactic:
simp_rw [preimage_iUnion, nhdsSet_iUnion, comap_iSup, nhdsSet_singleton]

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ ⨆ i ∈ s, comap f (𝓝 i) ≤ ⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i})
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ AccPt x (comap f l) ↔ AccPt (f x) l

Tactic:
accPt_iff_clusterPt,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l

Tactic:
accPt_iff_clusterPt,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
nhdsWithin_inter,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s] a ⊓ 𝓝[t] a = 𝓝[t] a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (range (Pi.map f))

Tactic:
Set.range_piMap

Goal state after:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (univ.pi fun i ↦ range (f i))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅ → IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
· intro H
      simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
      exact H.1.prod H.2

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
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) →
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
· intro h t ht
    rcases h t ht with ⟨u, u_open, hu⟩
    rw [inter_comm, hu]
    apply IsOpen.inter u_open hs

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

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)

Tactic:
by
  rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ (s ↓∩ t).Nonempty

Tactic:
obtain ⟨x, hx⟩ := hs t ht ht'
    simpa using ⟨⟨x, hx.2⟩, hx.1⟩

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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ closure[inst✝] (range f) ⊆ C

Tactic:
C_closed.closure_subset_iff,

Goal state after:
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ range f ⊆ C
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint C (range g)

Tactic:
← image_univ,

Goal state after:
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint C (g '' univ)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
by
  rw [← continuousOn_univ, ← hs']
  exact ContinuousOn.iUnion_of_isOpen hf hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s},
    IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] s

Tactic:
rintro s ⟨t, i, ht, rfl⟩

Goal state after:
case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
⊢ IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] ((↑i).pi t)
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
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (sᶜ ∉ (↑f).bind fun x ↦ ↑(m x)) ↔ s ∈ (↑f).bind fun x ↦ ↑(m x)

Tactic:
by
    simp only [mem_bind', mem_coe, ← compl_mem_iff_notMem, compl_ofPred, compl_compl]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (comap (f ∘ Sigma.mk i) (𝓝 (f ⟨i, x⟩))) = comap f (𝓝 (f ⟨i, x⟩))

Tactic:
← comap_comap,

Goal state after:
case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (comap (Sigma.mk i) (comap f (𝓝 (f ⟨i, x⟩)))) = comap f (𝓝 (f ⟨i, x⟩))
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)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
choose f hf using fun b : B => b.2.2

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
by rwa [← subset_interior_iff_mem_nhdsSet]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst✝] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst✝¹] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
have XZ_in_U : π '' Z ⊆ U := (Set.image_mono Z_in_W).trans (image_preimage_subset π U)

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst✝] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst✝¹] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
XZ_in_U : π '' Z ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
choose t ht hsub using fun n =>
    ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

Tactic:
by
  refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩
  simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]
  exact fun h a b hb hba ha ↦ h hb <| ht hba ha

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

Goal state before:
pp: case refine_2
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty
⊢ (⋂₀ Q).Nonempty

Tactic:
exact hP hQP (hQ.image _)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
accPt_iff_clusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (f a))

Tactic:
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)

Goal state after:
case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ closure[inst✝²] {a | p a}] a) (𝓝 (f a))
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (g a))

Tactic:
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)

Goal state after:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous[inst✝², inst✝¹] f
hg : ¬p → Continuous[inst✝², inst✝¹] g
⊢ Continuous[inst✝², inst✝¹] fun a ↦ if p then f a else g a

Tactic:
split_ifs with h
  exacts [hf h, hg h]

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

Goal state before:
pp: case a.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

Tactic:
rsuffices ⟨x, hx⟩ : ∃ x, (s : Set X) = {x}
    · exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩
    refine minimal_nonempty_open_eq_singleton ho hne ?_
    refine fun t hts htne hto => of_not_not fun hts' => ht ?_
    lift t to Finset X using s.finite_toSet.subset hts
    exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩

Goal state after:
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
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y

Tactic:
lift x to s using hxs

Goal state after:
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