mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
l₁ l₂ : A ⟶ X
⊢ l₁ ≫ f = g → l₂ ≫ f = g → l₁ = l₂

Tactic:
h₁

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
l₁ l₂ : A ⟶ X
h₁ : l₁ ≫ f = g
⊢ l₂ ≫ f = g → l₁ = l₂
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ (X : WalkingParallelFamily (ULift.{w, 0} Bool)),
    (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
            X) ≫
        (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
          ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
            X) =
      𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj X)

Tactic:
rintro (_ | _)

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          zero) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          zero) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj zero)

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          one) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          one) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj one)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
l₁ l₂ : Y ⟶ A
⊢ f ≫ l₁ = g → f ≫ l₂ = g → l₁ = l₂

Tactic:
h₁

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
l₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
⊢ f ≫ l₂ = g → l₁ = l₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∘
        ⇑(ConcreteCategory.hom (↾Sum.inl))))
    (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))

Tactic:
Set.range_comp,

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)))
    (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
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' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'

Tactic:
rw [← sub_eq_zero, ← map_sub]

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' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) (r - r') = 0
Module: Mathlib.Data.Nat.Cast.Field

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

Tactic:
rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
by
  rw [← prod_atTop_atTop_eq] at hp
  exact hp.curry

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
p : ℕ
⊢ p ∈ n.factorization.support → φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
hp

Goal state after:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inl
d d' : ℕ
hn : 2 * (0 ^ 2 + d + 1) ≤ 2 * (0 ^ 2 + d + 1) + d'
⊢ 0 ^ (2 * (0 ^ 2 + d + 1) + d') < (2 * (0 ^ 2 + d + 1) + d' - d)!

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 + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
· simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]

Goal state after:
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 + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s

Tactic:
rintro (_ | _)

Goal state after:
case false
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif false then f else g).lift' s = bif false then f.lift' s else g.lift' s

case true
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif true then f else g).lift' s = bif true then f.lift' s else g.lift' s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s

Tactic:
rintro (_ | _) <;> rfl

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 : α
⊢ (∃ z, b = a + z • p) → toIcoMod hp a b = a

Tactic:
by
      rintro ⟨n, rfl⟩
      rw [toIcoMod_add_zsmul, toIcoMod_apply_left]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)

Tactic:
by
  simp [closure_eq_compl_interior_compl, hs.interior_biInter]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense (closure s) ↔ Dense s

Tactic:
by
  rw [Dense, Dense, closure_closure]

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
sdiff_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ (interior s)ᶜ = closure s ∩ (interior s)ᶜ
Module: Mathlib.Topology.ClusterPt

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

Tactic:
sdiff_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C ∩ {x}ᶜ))
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ¬x ∉ interior s

Tactic:
not_not

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ x ∈ interior s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
h : btw (↑z✝) x₂ x₃
⊢ btw x₂ x₃ ↑z✝

Tactic:
induction x₂ using QuotientAddGroup.induction_on

Goal state after:
case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h : btw (↑z✝¹) (↑z✝) x₃
⊢ btw (↑z✝) x₃ ↑z✝¹
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ x₄ : α ⧸ AddSubgroup.zmultiples p
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
z✝ : α
h₁₂₃ : btw (↑z✝) x₂ x₃ ∧ ¬btw x₃ x₂ ↑z✝
⊢ btw (↑z✝) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝

Tactic:
induction x₂ using QuotientAddGroup.induction_on

Goal state after:
case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ x₄ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h₂₃₄ : btw (↑z✝) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝
h₁₂₃ : btw (↑z✝¹) (↑z✝) x₃ ∧ ¬btw x₃ ↑z✝ ↑z✝¹
⊢ btw (↑z✝¹) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝¹
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
h₁₂₃ : btw (↑z✝) x₂ x₃
h₃₂₁ : btw x₃ x₂ ↑z✝
⊢ ↑z✝ = x₂ ∨ x₂ = x₃ ∨ x₃ = ↑z✝

Tactic:
induction x₂ using QuotientAddGroup.induction_on

Goal state after:
case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h₁₂₃ : btw (↑z✝¹) (↑z✝) x₃
h₃₂₁ : btw x₃ ↑z✝ ↑z✝¹
⊢ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = x₃ ∨ x₃ = ↑z✝¹
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
⊢ btw (↑z✝) x₂ x₃ ∨ btw x₃ x₂ ↑z✝

Tactic:
induction x₂ using QuotientAddGroup.induction_on

Goal state after:
case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
⊢ btw (↑z✝¹) (↑z✝) x₃ ∨ btw x₃ ↑z✝ ↑z✝¹
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Icc (↑n) (↑n + 1) = univ

Tactic:
by
  simpa only [zero_add] using iUnion_Icc_add_intCast (0 : α)

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

Goal state before:
pp: A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ IsOpen[inst✝²] (p ⁻¹' U) ↔ ∃ V, IsOpen[inst✝] V ∧ g ⁻¹' V = U

Tactic:
hf.isOpen_iff,

Goal state after:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ V, IsOpen[inst✝] V ∧ g ⁻¹' V = U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : {u | GenerateOpen s u} = s
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] = IsOpen[generateFrom s]

Tactic:
ext U; exact Set.ext_iff.mp hs.symm U

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) l
⊢ (𝓝 x ⊓ comap f l).NeBot

Tactic:
← map_neBot_iff,

Goal state after:
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) l
⊢ (map ?f (𝓝 x ⊓ comap f l)).NeBot

case f
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) l
⊢ X → ?m.18

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) l
⊢ Type ?u.31
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
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ¬¬ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ ¬¬ClusterPt x (𝓟 sᶜ)

Tactic:
not_not

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ ClusterPt x (𝓟 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 : IsClosedEmbedding g
⊢ IsEmbedding f ∧ IsClosed[inst✝] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst✝¹] (range f)

Tactic:
Set.range_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 : IsClosedEmbedding g
⊢ IsEmbedding f ∧ IsClosed[inst✝] (g '' range f) ↔ IsEmbedding f ∧ IsClosed[inst✝¹] (range f)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ Tendsto f (𝓝[≠] a) (𝓝 (f a))

Tactic:
by
  simp [ContinuousAt, -pure_sup_nhdsNE, ← pure_sup_nhdsNE a, tendsto_pure_nhds]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ

Tactic:
sUnion_image,

Goal state after:
case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃ a ∈ {f | f.Finite ∧ f ⊆ s}, ⋂₀ a = univ
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsCoinducing (s.restrictPreimage f)

Tactic:
by
  refine .of_isOpen_preimage_iff_isOpen fun _ ↦ ?_
  rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : u ∈ ⋃ i, image Subtype.val '' b i
⊢ IsOpen[t] u

Tactic:
simp only [mem_iUnion, mem_image] at hu
    rcases hu with ⟨i, s, sb, rfl⟩
    exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : (↑s).pi U = ∅
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

pp: case inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
· simp [h]

Goal state after:
case inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)
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
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Tactic:
refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩

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)
this : Countable ↑B
⊢ ∀ t' ∈ range fun i ↦ s i, t' ⊆ ⋃ i ∈ range f, s i
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
rw [nhds_pi, Filter.mem_pi] at hn
    obtain ⟨s, -, n', hn', hsub⟩ := hn
    choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
    refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩
    · exact (set_pi_mem_nhds_iff (@Set.finite_univ ι _) _).mpr fun i _ => hn'' i
    · exact fun i _ => hsub' i (h i trivial)

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ⇑e)
⊢ LocallyFinite f

Tactic:
simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)

Tactic:
← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff,

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite (f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ↔ LocallyFinite (f ∘ some)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
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 ∈ image π '' V, IsOpen[inst✝] u

Tactic:
rintro - ⟨U, U_in_V, rfl⟩

Goal state after:
case h_open
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 X
U_in_V : U ∈ V
⊢ IsOpen[inst✝] (π '' U)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
⊢ SigmaCompactSpace X

Tactic:
rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩

Goal state after:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s✝ t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : ⋃ x ∈ s, K x = univ
⊢ SigmaCompactSpace X
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
by simpa [f] using hnhds

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
by
    obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
    exact ⟨Set.image π '' V, V_countable.image (Set.image π),
      (V_generates.isQuotientMap h' h).eq_generateFrom⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
refine (forall_neBot_le_iff ?_).trans ?_

Goal state after:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Monotone fun f ↦ ∃ x ∈ s, ClusterPt x f

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x ↑f) ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x