mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ (X : GrpCat),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X)))) =
      𝟙 (CommGrpCat.of (Abelianization ↑X))

Tactic:
intros
    ext : 1
    apply (Equiv.eq_symm_apply Abelianization.lift).mp
    rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X Y Z : GrpCat} (f : X ⟶ Y) (g : Y ⟶ Z),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f ≫ g)))) =
      CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f))) ≫
        CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g)))

Tactic:
intros
    ext : 1
    apply (Equiv.eq_symm_apply Abelianization.lift).mp
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case pos
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inl) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, ⋯⟩))

Tactic:
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case neg
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ¬∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inr) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))

Tactic:
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
x : α
⊢ f (x - c) = -f x

Tactic:
by simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)

Tactic:
simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r • y ∈ (extensionOfMax i f).domain

Tactic:
eq1

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
⊢ 0 ∈ (extensionOfMax i f).domain
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case convert_2
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
⊢ r • y = r' • y

Tactic:
eq1

Goal state after:
case convert_2
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
⊢ r' • y = r' • y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ n.divisors.sum φ = n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

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

case inr
n : ℕ
hn : n > 0
⊢ n.divisors.sum φ = n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
have : n = ∑ d ∈ n.divisors, #{k ∈ range n | n.gcd k = d} := by
    nth_rw 1 [← card_range n]
    refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
    apply gcd_dvd_left

Goal state after:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    {x ∈ range (p ^ (n + 1)) | x ∉ image (fun x ↦ x * p) (range (p ^ n))}

Tactic:
apply filter_congr

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun x ↦ x * p) (range (p ^ n))
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Goal state after:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop (atTop ×ˢ atTop)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2

Tactic:
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩

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

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Goal state after:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ atTop.IsCountablyGenerated

Tactic:
rw [← prod_atTop_atTop_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ (atTop ×ˢ atTop).IsCountablyGenerated
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n

Tactic:
rw [totient_mul _, totient_prime hp]

Goal state after:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n
Module: Mathlib.Data.Nat.Totient

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

Tactic:
by
    rw [← mul_assoc, mul_comm a] at h'
    exact h'.not_lt this

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

Goal state before:
pp: case neg.refine_1
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)

Tactic:
rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]
    · exact hp.one_lt
    · exact totient_pos.mpr <| pos_of_ne_zero ha

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

Tactic:
by
  rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]
  exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

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

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

Tactic:
toIcoDiv_add_zsmul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a b + m = m + toIcoDiv hp 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 : α
m : ℤ
⊢ toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m

Tactic:
toIcoDiv_add_zsmul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a b + -m = toIcoDiv hp a b - m
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_eq_add]

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

Tactic:
toIcoDiv_add_zsmul,

Goal state after:
α : 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 = toIcoMod hp a b
Module: Mathlib.Topology.Basic

Goal state before:
pp: case insert
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → IsOpen[inst✝] (⋂₀ s✝)
h : ∀ t ∈ insert a✝¹ s✝, IsOpen[inst✝] t
⊢ IsOpen[inst✝] (⋂₀ insert a✝¹ s✝)

Tactic:
| insert _ _ ih =>

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
rw [← closure_subset_iff_isClosed]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (frontier s)

Tactic:
by
  rw [frontier_eq_closure_inter_closure]; exact IsClosed.inter isClosed_closure isClosed_closure

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst✝¹, inst✝] f
⊢ ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)

Tactic:
exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
rw [continuous_iff_coinduced_le] at h₂ ⊢

Goal state after:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))

Tactic:
ext s

Goal state after:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
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
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (𝓝ˢ s) = 𝓝ˢ (f '' s)

Tactic:
rw [← biUnion_of_singleton s]
  simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]

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
s : Set Y
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Tactic:
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using!
    inter_subset_inter hf.preimage_closure_subset_closure_preimage
      hf.preimage_closure_subset_closure_preimage

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.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
by haveI := ta1; haveI := tb1; exact Continuous 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 α
a : α
⊢ 𝓝[∅] a = ⊥

Tactic:
by rw [nhdsWithin, principal_empty, inf_bot_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : IndiscreteTopology X
hY : IndiscreteTopology Y
⊢ induced fst inst✝¹ = ⊤ ∧ induced snd inst✝ = ⊤

Tactic:
simp [h.eq_top, hY.eq_top]

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

Goal state before:
pp: Y : Type v
W : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ instTopologicalSpaceProd = induced (fun p ↦ (f p.1, g p.2)) instTopologicalSpaceProd

Tactic:
by
  delta instTopologicalSpaceProd
  simp_rw [induced_inf, induced_compose]
  rfl

Goal state after:
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
ext s

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s✝ s : Set α
⊢ s ∈ 𝓝ˢ s✝ ↔ s ∈ comap f (𝓝ˢ (f '' s✝))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
h : IsClosedMap f
⊢ (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)

Tactic:
exact ⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
by
  refine
    ⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
  obtain ⟨t, ht, hts⟩ := h hs.compl
  rw [subset_compl_comm, ← preimage_compl] at hts
  exact (IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u : Set β
h : u ∈ 𝓝ˢ t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s] (s ∩ f ⁻¹' t)

Tactic:
simpa [h] using ContinuousOn.preimage_mem_nhdsSetWithin hf (t := t) (u := u) (t' := univ)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ x ∈ Subtype.val '' t, f x
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case refine_1
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)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ univ.pi n'' ∈ 𝓝 t

pp: case refine_2
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)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
h : x✝ ∈ univ.pi n''
⊢ x✝ ∈ s.pi n'

Tactic:
· exact (set_pi_mem_nhds_iff (@Set.finite_univ ι _) _).mpr fun i _ => hn'' i

Goal state after:
case refine_2
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)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
h : x✝ ∈ univ.pi n''
⊢ x✝ ∈ s.pi n'
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s

Tactic:
smallSets,

Goal state after:
α : Type u_1
f : Filter α
⊢ f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ ⊥.smallSets = pure ∅

Tactic:
smallSets,

Goal state after:
α : Type u_1
⊢ ⊥.lift' powerset = pure ∅
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ ⊤.smallSets = ⊤

Tactic:
smallSets,

Goal state after:
α : Type u_1
⊢ ⊤.lift' powerset = ⊤
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
by_cases hx : x ∈ closure (f i)

Goal state after:
case pos
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
this : IsClosed[inst✝] (⋃ i, f ↑i)
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite fun n ↦ {x | f (n + 1) x ≠ f n x}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
choose U hUx hU using hf
  choose N hN using fun x => (hU x).bddAbove
  replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y :=
    fun x n hn y hy => by_contra fun hne => hn.lt.not_ge <| hN x ⟨y, hne, hy⟩
  replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y :=
    fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
  refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
  filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]
  rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩
  calc
    f n y = f (N x + 1) y := hN _ _ hn _ hy
    _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
    _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

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
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
have := calc
    ⋃ i, s i
    _ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
    _ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
    _ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']

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
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ i, s i)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ x ∈ f '' s, ClusterPt x l

Tactic:
have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ f '' s, ClusterPt x l
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ Minimal (fun x ↦ x ∈ upperClosure s) x ↔ x ∈ s

Tactic:
by
  simp only [upperClosure]
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
  · obtain ⟨a, has, hax⟩ := h.prop
    rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]
  rwa [← hs.eq has h (hab.trans hbx)]

Goal state after: