mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
lt_iff_le_not_ge

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ (a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
· exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)

Goal state after:
case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x - n • c) = ↑n.negOnePow • f x

Tactic:
simpa only [sub_eq_add_neg, neg_zsmul, Int.negOnePow_neg] using h.add_zsmul_eq (-n)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ n

Tactic:
count_eq_card_filter_range

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case convert_2
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 < p ^ t * (k + 2)

Tactic:
simp [htp.ne', hp.one_lt]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ count p n ≤ #hp.toFinset

Tactic:
count_eq_card_filter_range

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #hp.toFinset
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a n : ℕ
⊢ count (fun x ↦ a.Coprime x) a = #({a_1 ∈ range a | a.Coprime a_1})

pp: case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a

Tactic:
count_eq_card_filter_range

Goal state after:
a n : ℕ
⊢ #({x ∈ range a | a.Coprime x}) = #({a_1 ∈ range a | a.Coprime a_1})

case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a
Module: Mathlib.Data.Nat.Totient

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

Tactic:
by
      have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
      have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a => by
        simp only [mem_image, mem_range, exists_imp]
        rintro b ⟨h, rfl⟩
        rw [Nat.pow_succ]
        exact (mul_lt_mul_iff_left₀ hp.pos).2 h
      rw [card_sdiff_of_subset h2, Finset.card_image_of_injective _ h1, card_range, card_range, ←
        one_mul (p ^ n), pow_succ', ← tsub_mul, one_mul, mul_comm]

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

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
· simp [hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

pp: case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
· rw [← pow_mul, ← pow_add]
    congr 1
    lia

Goal state after:
case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
· simp [hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (p * a * d)

Tactic:
rw [mul_comm p]

Goal state after:
case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p * d)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p

Tactic:
convert! toIcoMod_mem_Ico hp 0 b
  exact (zero_add p).symm

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

Tactic:
refine toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_
  rw [sub_smul, ← sub_add, add_right_comm]
  simpa using sub_toIcoDiv_zsmul_mem_Ico hp a b

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

Tactic:
rw [toIocMod, toIocDiv_add_zsmul, toIocMod, add_smul]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
sup_le_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : x ∈ closure[inst✝] (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure[inst✝] s₂

Tactic:
mem_closure_iff_nhds_ne_bot

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
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 : ℤ
⊢ toIocMod hp a (b - ↑m * p) = toIocMod hp a b

Tactic:
simpa using toIocMod_sub_zsmul hp a b m

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)

Tactic:
Set.mem_Ico,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a ≤ b - ⌊(b - a) / p⌋ • p ∧ b - ⌊(b - a) / p⌋ • p < a + p
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsClosed[inst✝] s
⊢ ∃ c, IsClosed[inst✝¹] c ∧ f '' s = c ∩ range f

Tactic:
obtain ⟨c, hc, rfl⟩ := hf.isClosed_iff.1 hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
c : Set Y
hc : IsClosed[inst✝¹] c
hs : IsClosed[inst✝] (f ⁻¹' c)
⊢ ∃ c_1, IsClosed[inst✝¹] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous[t₁, iInf t₂] f ↔ ∀ (i : ι), Continuous[t₁, t₂ i] f

Tactic:
by
  simp only [continuous_iff_coinduced_le, le_iInf_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s

Tactic:
mem_nhds_iff,

Goal state after:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t ⊆ s, IsOpen[induced f T] t ∧ a ∈ t) ↔ ∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
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
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)

Tactic:
rw [IsOpenMap, compl_surjective.forall]
  simp [kernImage_eq_compl]

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
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
rw [isClosedMap_iff_closure_image, compl_surjective.forall]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set X), closure[inst✝] (f '' xᶜ) ⊆ f '' closure[inst✝¹] xᶜ) ↔
    ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
  simp only [eventually_nhdsWithin_iff] at h ⊢
  exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v

Tactic:
simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto (t.piecewise f g) (𝓝[s] a) l

Tactic:
by
  apply Tendsto.piecewise <;> rwa [← nhdsWithin_inter']

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
have : ∀ t, IsOpen (s.domRestrict f ⁻¹' t) ↔ ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isOpen_induced_iff, Set.domRestrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
    constructor <;>
      · rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
  rw [continuousOn_iff_continuous_domRestrict, continuous_def]; simp only [this]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Tactic:
mem_nhds_iff,

Goal state after:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, IsOpen t ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
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
B : Disjoint C (range g)
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
exact B.mono_left A

Goal state after:
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:
by
  rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
by
  cases nonempty_fintype ι
  rw [isOpen_iff_nhds]
  simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
  refine forall₂_congr fun a _ => ⟨?_, ?_⟩
  · rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
    rw [← pi_inter_compl (I : Set ι)]
    exact inter_subset_left
  · exact fun ⟨u, ⟨h1, _⟩⟩ =>
      ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := ⋯
this : f.NeBot
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g

Tactic:
calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
⊢ ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
    refine ⟨U, hUo, ?_⟩
    simpa [Set.ext_iff] using hU

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)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Countable ↑B
i : ι
x : α
xs : x ∈ (fun i ↦ s i) i
b : Set α
hb : b ∈ countableBasis α
xb : x ∈ b
bs : b ⊆ (fun i ↦ s i) i
⊢ x ∈ ⋃ i ∈ range f, s i

Tactic:
exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
simpa using this

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] a = 𝓝[⋃ i, f i ∩ U] a

Tactic:
by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, K i n = ⋃ i, ⋃ n, Function.uncurry K (i, n)

Tactic:
Function.uncurry_def

Goal state after:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, K i n = ⋃ i, ⋃ n, (fun p ↦ K p.1 p.2) (i, n)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
i : ι
hi : i ∈ {i | y ∈ s i}
hy : ∀ (i : ι), x ∉ s i → y ∉ s i
⊢ i ∈ {i | x ∈ s i}

Tactic:
exact not_imp_not.mp (hy i) hi

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i : ι
⊢ (t i₀ ∩ t i).Nonempty

Tactic:
rcases htd i₀ i with ⟨j, hji₀, hji⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i j : ι
hji₀ : t i₀ ⊇ t j
hji : t i ⊇ t j
⊢ (t i₀ ∩ t i).Nonempty
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
t t' : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) = 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
by
  simp [nhdsSetWithin, ← prod_inf_prod, hs.nhdsSet_prod_eq ht]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
h : y ∈ closure[inst✝] {x}
⊢ ∀ (i' : Set X), y ∈ i' ∧ IsOpen[inst✝] i' → i' ∈ 𝓝 x

Tactic:
rintro s ⟨hy, ho⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
h : y ∈ closure[inst✝] {x}
s : Set X
hy : y ∈ s
ho : IsOpen[inst✝] s
⊢ s ∈ 𝓝 x
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t

Tactic:
ite_inter_self,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
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
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y

Tactic:
exact congr_arg Subtype.val hxy.eq

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → s_1.Finite → s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s

Tactic:
intro τ t hτ h₁t h₂t

Goal state after:
case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
h₂t : tᶜ ∈ codiscreteWithin s
⊢ (insert τ t)ᶜ ∈ codiscreteWithin s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert.refine_1.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
t : Finset ι
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hx : i ∉ t
hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U i) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
h2K₁ : K₁ ⊆ U i
⊢ IsCompact (update K i K₁ i)

Tactic:
simp only [update_self, h1K₁]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
exact fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

Goal state after: