mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
⊢ IsIso (Abelian.coimageImageComparison f)

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
this : PreservesColimits G
⊢ IsIso (Abelian.coimageImageComparison f)
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : ((i ≫ h) ≫ e) ≫ i = i
⊢ a = default
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Tactic:
refine ⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) PUnit.unit ≫
      G.map (((Adjunction.ofIsRightAdjoint G).homEquiv A B).symm h) =
    h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCoseparator (unop G) ↔ IsSeparator G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else ⋯.choose) ^ n✝ = a

Tactic:
dsimp only

Goal state after:
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else ⋯.choose) ^ n✝ = a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)

Tactic:
induction n

Goal state after:
case zero
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
⊢ Periodic f (0 • c)

case succ
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n✝ : ℕ
a✝ : Periodic f (n✝ • c)
⊢ Periodic f ((n✝ + 1) • c)
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c d : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b →
    b < d ∧ d < c ∨ d < c ∧ c < b ∨ c < b ∧ b < d → a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩) <;>
      first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
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.inr (Or.inl ⟨hcb, hba⟩)

Goal state after:
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.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (a + ↑n) (a + ↑n + 1))

Tactic:
by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ico_add_zsmul a (1 : α)

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

Goal state before:
pp: a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
⊢ Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
hp'

Goal state after:
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
⊢ ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case univ
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q

Tactic:
exact Or.inl cond.univ_mem

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
intro N
  obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
    exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
  have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
  obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
      ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k := by
    rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
    push Not at hn_min
    exact ⟨n, hnN, hnk, hn_min⟩
  use n, hnN
  grind

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
nth_rw 3 [← prod_factorization_pow_eq_self hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)
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 : ℤ
⊢ b + m • p - (toIcoDiv hp a b + m) • p ∈ Set.Ico a (a + p)

Tactic:
by
    simpa only [add_smul, add_sub_add_right_eq_sub] 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 : α
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Tactic:
by
  rw [add_comm, toIcoDiv_add_right']

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed s

Tactic:
rw [subset_closure.antisymm h]; exact isClosed_closure

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
U : Set X
U_op : IsOpen U
x : X
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
exact mem_closure_iff.1 (h _) U U_op x_in

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 t_1 : Set X),
    (∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = s) →
      (∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1) → ∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = s ∩ t_1

Tactic:
rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
s'₁ : Set Y
hs₁ : IsOpen[t] s'₁
s'₂ : Set Y
hs₂ : IsOpen[t] s'₂
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = f ⁻¹' s'₁ ∩ f ⁻¹' s'₂
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 : α
⊢ toIcoMod hp a b = a + Int.fract ((b - a) / p) * p

Tactic:
by
  rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]
  simp [field, -Int.self_sub_floor]
  ring

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
rw [Set.inter_union_compl s t]

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
⊢ TopologicalSpace.coinduced p inst✝² = TopologicalSpace.induced g inst✝

Tactic:
ext U

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
⊢ IsOpen[TopologicalSpace.coinduced p inst✝²] U ↔ IsOpen[TopologicalSpace.induced g inst✝] U
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp
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) → ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
rintro ⟨V, hV, e⟩
    refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩
    ext x
    obtain ⟨x, rfl⟩ := hp x
    constructor
    · rintro ⟨y, hy, e'⟩
      obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
      rw [← hg ((congr_fun h y).trans e')]
      exact e.le hy
    · intro H
      exact ⟨f x, e.ge H, congr_fun h.symm x⟩

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
by
  simp only [nhds_generateFrom, @forall_comm (b ∈ _), tendsto_iInf, mem_ofPred_eq, and_imp,
    tendsto_principal]; rfl

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

Goal state after:
α : Type u
s : Set (Set α)
hs : {u | GenerateOpen s u} = s
U : Set α
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → IsOpen[t₁] s

Tactic:
by
  rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]
  exact fun hs a ha => h _ (hs _ ha)

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ ¬induced ofTopology t = ⊤ ↔ ¬t = ⊤

Tactic:
not_iff_not

Goal state after:
α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ ↔ t = ⊤
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ sᶜᶜ = (s ∪ t)ᶜᶜ ∩ vᶜ

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t)ᶜᶜ ∩ vᶜ
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t)ᶜᶜ ∩ vᶜ

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t) ∩ vᶜ
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
f : X → Y
inst✝ : IndiscreteTopology Y
hf : IsInducing f
⊢ inst✝¹ = ⊤

Tactic:
let : TopologicalSpace Y := ⊤

Goal state after:
case refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
f : X → Y
inst✝ : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
⊢ inst✝¹ = ⊤
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
by
  classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_continuous_injective_isOpenMap, ← hg.isOpenMap_iff, ←
    hg.1.continuous_iff, hg.injective.of_comp_iff]

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.29
Y : Type ?u.32
Z : Type ?u.38
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
⊢ Sort ?u.55

Tactic:
haveI := sInf tas; haveI := sInf tbs
    exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure[inst✝] (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[≠] z, x ∈ s

Tactic:
by
  simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

Goal state after:
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)
⊢ DenseRange (Pi.map f)

Tactic:
rw [DenseRange, Set.range_piMap]
  exact dense_pi Set.univ (fun i _ => hf i)

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
⊢ 𝓝 x = pure x ⊔ cofinite

Tactic:
ext U

Goal state after:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
simp_rw [mem_nhdsSet_iff_exists, isOpen_induced_iff]

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t u : Set ↑s
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val '' u ∈ 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
← map_nhdsSet_subtype_val,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t u : Set ↑s
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val '' u ∈ map Subtype.val (𝓝ˢ t)
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
⊢ IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Tactic:
by
  simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃ i, ↑i

Tactic:
← sUnion_eq_iUnion

Goal state after:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst✝] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst✝] (f '' ⋃₀ {s | s ∈ B ∧ s ⊆ o})

Tactic:
sUnion_eq_iUnion,

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst✝] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst✝] (f '' ⋃ i, ↑i)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x ⊆ ⋃ x, s x

pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, accumulate s x

Tactic:
· simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
    intro z x x' ⟨_, hz⟩
    exact ⟨x', hz⟩

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, accumulate s x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (⋃ i, s i)

Tactic:
choose c hc h'c using hs

Goal state after:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure[t] (c i)
⊢ IsSeparable (⋃ i, s i)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace

Tactic:
refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
    simp [hs]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case neg
ι : 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
hi : i ∉ s
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
· rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn
    exact ⟨b, ht.2.2⟩

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ l.smallSets.NeBot

Tactic:
refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty
  exact monotone_powerset

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ∩ f '' s = L n

Tactic:
inter_eq_left.mpr

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n = L n

X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ x ∈ K n ↔ K.find x ≤ n

Tactic:
by
  classical
  exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ (lowerBounds ↑(upperClosure s)).Nonempty ↔ (lowerBounds s).Nonempty

Tactic:
lowerBounds_upperClosure

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
⊢ (map f).symm = map f.symm

Tactic:
ext; simp [map, OrderIso.symm_apply_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
obtain ⟨s', hs', u, hu, h⟩ := hn

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
s' : Set X
hs' : s' ∈ 𝓟 s
u : Set Y
hu : u ∈ 𝓝ˢ[t'] t
h : s' ×ˢ u ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
by
  tfae_have 1 → 2 := (pure_le_nhds _).trans
  tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
  tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
  tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
  tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff
  tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]
  tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs
  tfae_finish

Goal state after: