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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ IsSeparator (AddCommGrpCat.of (ULift.{u, 0} ℤ))

Tactic:
intro A

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A : AddCommGrpCat
⊢ ∀ ⦃Y : AddCommGrpCat⦄ (f g : A ⟶ Y),
    (∀ (G : AddCommGrpCat),
        ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g) →
      f = g
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
by
  rcases n with n | n
  · simpa only [Int.ofNat_eq_natCast, natCast_zsmul] using h.nsmul n
  · simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddZeroClass α
h : Periodic f c
⊢ f c = f 0

Tactic:
simpa only [zero_add] using h 0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddZeroClass α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f c = -f 0

Tactic:
simpa only [zero_add] using h 0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝² : Add α
inst✝¹ : IsRightCancelAdd α
inst✝ : SubtractionCommMonoid β
hf : Antiperiodic f c
s : Finset α
⊢ ∑ k ∈ Finset.map (addRightEmbedding c) s, f k = -∑ k ∈ s, f k

Tactic:
simp [hf _]

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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r

Tactic:
unfold ExtensionOfMaxAdjoin.extensionToFun

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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
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
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
unfold ExtensionOfMaxAdjoin.extensionToFun

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
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b))
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case neg.refine_2
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
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ (p ^ n).Coprime a

Tactic:
simpa [hn, Prime.coprime_iff_not_dvd hp']

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

Goal state before:
pp: case zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
⊢ motive (p ^ 0 * a)

Tactic:
simpa using ha

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

Goal state before:
pp: case a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False

Tactic:
rw [totient_one, tsub_self] at h

Goal state after:
case a
hp : 0 < 1
h : 1 = 0
⊢ False
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[inst✝] sᶜᶜ ↔ IsOpen[inst✝] s

Tactic:
compl_compl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ ⊥.lift' h = 𝓟 (h ∅)

Tactic:
by
  rw [← principal_empty, lift'_principal hh]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense sᶜᶜ

Tactic:
compl_compl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense s
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 : α
⊢ [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE

Tactic:
by
  rw [modEq_iff_toIcoMod_eq_left hp]
  tfae_have 3 → 2 := by
    rw [← not_exists, not_imp_not]
    exact fun ⟨i, hi⟩ =>
      ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
        ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm
  tfae_have 4 → 3
  | h => by
    rw [← h, Ne, eq_comm, add_eq_left]
    exact hp.ne'
  tfae_have 1 → 4
  | h => by
    rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
    refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
    rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
    conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
  tfae_have 2 → 1 := by
    rw [← not_exists, not_imp_comm]
    have h' := toIcoMod_mem_Ico hp a b
    exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
  tfae_finish

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
x₁ x₂ x₃ : α
h : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
let x₂' := toIcoMod hp x₁ x₂
  let x₃' := toIcoMod hp x₂' x₃
  have h : x₂' ≤ toIocMod hp x₁ x₃' := by simpa [x₃']
  have h₂₁ : x₂' < x₁ + p := toIcoMod_lt_right _ _ _
  have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (toIcoMod_lt_right _ _ _)
  suffices hequiv : x₃' ≤ toIocMod hp x₂' x₁ by
    obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
    simpa [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_right]
  rcases le_or_gt x₃' (x₁ + p) with h₃₁ | h₁₃
  · suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge h₃₁
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨h₂₁, by simp [x₂', left_le_toIcoMod]⟩, -1, by simp⟩
  have hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p := by
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 1, by simp⟩
  have not_h₃₂ := (h.trans hIoc₁₃.le).not_gt
  contradiction

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 : α
⊢ toIcoDiv hp a b = ⌊(b - a) / p⌋

Tactic:
by
  refine toIcoDiv_eq_of_sub_zsmul_mem_Ico hp ?_
  rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
    sub_right_comm _ _ a]
  exact ⟨Int.sub_floor_div_mul_nonneg _ hp, Int.sub_floor_div_mul_lt _ hp⟩

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 ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)

Tactic:
by rw [nhdsSet_union]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
U : Set X
U_open : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝] (f '' U)

Tactic:
by
    obtain ⟨V, hV, rfl⟩ := ind.isOpen_iff.mp U_open
    rwa [V.image_preimage_eq surj]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.univ
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ univ = ∅ ∨ univ = univ

Tactic:
exact .inr rfl

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ Dense (range f) ↔ Surjective f

Tactic:
dense_discrete,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ range f = univ ↔ Surjective f
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]

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

Goal state before:
pp: Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (comap g (𝓝 (g y))) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
tendsto_comap_iff

Goal state after:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto (g ∘ f) l (𝓝 (g y)) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
a : α
⊢ 𝓝 a = ⊤

Tactic:
by
  cases IndiscreteTopology.eq_top α
  exact nhds_top

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h.symm ⁻¹' interior s = interior (⇑h.symm ⁻¹' s)

Tactic:
preimage_interior

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ interior (⇑h.symm ⁻¹' s) = interior (⇑h.symm ⁻¹' s)
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
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.55

Tactic:
exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

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
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ sᶜᶜ = s

Tactic:
compl_compl

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ s = s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
⊢ 𝓝[⋃ i ∈ S, i] a = ⨆ s ∈ S, 𝓝[s] a

Tactic:
nhdsWithin_biUnion hS

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
⊢ ⨆ i ∈ S, 𝓝[i] a = ⨆ s ∈ S, 𝓝[s] a
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
X : Type u_5
s t : Set X
⊢ (s.Nonempty → sᶜ.Finite) → (t.Nonempty → tᶜ.Finite) → (s ∩ t).Nonempty → (s ∩ t)ᶜ.Finite

Tactic:
rintro hs ht ⟨x, hxs, hxt⟩

Goal state after:
X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
⊢ (s ∩ t)ᶜ.Finite
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (y : ↑s) in 𝓝 a, y ∈ J) ↔ ∃ᶠ (a : { x // x ∈ t }) in 𝓝 ⟨↑a, ⋯⟩, ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J

Tactic:
Topology.IsInducing.subtypeVal.nhds_eq_comap,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (y : ↑s) in comap Subtype.val (𝓝 ↑a), y ∈ J) ↔ ∃ᶠ (a : { x // x ∈ t }) in 𝓝 ⟨↑a, ⋯⟩, ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in 𝓝 ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔ ∃ᶠ (a : { x // x ∈ t }) in 𝓝 ⟨↑a, ⋯⟩, ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J

Tactic:
Topology.IsInducing.subtypeVal.nhds_eq_comap,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in 𝓝 ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (a : { x // x ∈ t }) in comap Subtype.val (𝓝 ↑⟨↑a, ⋯⟩), ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto f l (comap Subtype.val (𝓝 a)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Tactic:
tendsto_comap_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ↑⟨a, ha⟩)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ t₁ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
    ∀ t₂ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
      ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
    exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (⨅ s ∈ {s | a ∈ s ∧ s ∈ b}, 𝓟 s).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
biInf_sets_eq

Goal state after:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ ⋃ i ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 i).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn (𝓟 ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {s | a ∈ s ∧ s ∈ b}

case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case e'_3
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
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)

Tactic:
· rw [← disjoint_principal_left]
    exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
⊢ IsOpenMap (Pi.map f)

Tactic:
refine IsOpenMap.of_nhds_le fun x ↦ ?_

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ 𝓝 (Pi.map f x) ≤ map (Pi.map f) (𝓝 x)
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
⊢ sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
compl_compl

Goal state after:
α : Type u_2
x✝ : Bornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
⊢ Countable ι

Tactic:
by
  rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩
  choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)
  have f_inj : Injective f := fun i j hij ↦
    hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩
  have := u_countable.to_subtype
  exact (f_inj.codRestrict hfu).countable

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

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
compl_compl

Goal state after:
α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 s = ⊥
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
⊢ sᶜᶜ ∉ f ↔ s ∉ f

Tactic:
compl_compl

Goal state after:
α : Type u
f : Ultrafilter α
s : Set α
⊢ s ∉ f ↔ s ∉ f
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, s i = ⋃ i, ⋃ n, K i n

Tactic:
hcov

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
have : Countable ↑s := countable_coe_iff.mpr hc

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ i ∈ s, S i)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ s ∩ ⋃ i, K i = s

Tactic:
hcov

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ s ∩ t = s
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
⊢ (f ⁻¹' ⋃ n, L n) ∩ s = f ⁻¹' f '' s ∩ s

Tactic:
hcov

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
⊢ f ⁻¹' f '' s ∩ s = f ⁻¹' f '' s ∩ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : ↑f ≤ l
x : X
hxs : x ∈ s
hx : ↑f ≤ 𝓝 x
⊢ x ∈ s'

Tactic:
exact h x hxs (.mono (.of_le_nhds hx) hf)

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ IsCompact s

Tactic:
isCompact_iff_ultrafilter_le_nhds',

Goal state after:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ iᶜᶜ ∈ f) ↔ ∃ K ∈ f, IsCompact K

Tactic:
compl_compl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.erase a = s ↔ a ∉ s

Tactic:
rw [← sdiff_singleton]

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (closure[inst✝] sᶜᶜ) ↔ IsCompact (closure[inst✝] s)

Tactic:
compl_compl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (closure[inst✝] s) ↔ IsCompact (closure[inst✝] s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact univ

Tactic:
by
  rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
this : univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
by
    simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this

Goal state after: