mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) [inst : Mono f]
    {q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T}
    (hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f

Tactic:
intro P f hf q hq

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : { P // ∃ q, S.map P.arrow.unop ≫ q = A.hom }
⊢ ↑((fun P ↦ ⟨projectQuotient P, ⋯⟩) ((fun P ↦ liftQuotient ↑P ⋯) P)) = ↑P

Tactic:
by simp only [liftQuotient, Quiver.Hom.unop_op, homMk_left,
      Quiver.Hom.op_unop, projectQuotient_mk, Subobject.mk_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁴ : (coyoneda.obj (op G)).Faithful
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
hfg : ∀ (h : G ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝
⊢ (coyoneda.obj (op G)).map x✝¹ = (coyoneda.obj (op G)).map x✝

Tactic:
ext; apply hfg

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁴ : (yoneda.obj G).Faithful
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
hfg : ∀ (h : x✝² ⟶ G), x✝¹ ≫ h = x✝ ≫ h
⊢ (yoneda.obj G).map x✝¹.op = (yoneda.obj G).map x✝.op

Tactic:
ext; apply hfg

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
have := h X
    refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)
    simpa using hh j.as

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul] using h (a • x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = -(fun x ↦ f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul] using h (a • x)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b

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

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

pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p

Tactic:
· rwa [succ_le_iff]

Goal state after:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p
Module: Mathlib.Order.Filter.AtTopBot.Finite

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

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

Goal state after:
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 : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnotMem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False

Tactic:
exact hnotMem hmem

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)
  · simp [zero_dvd_iff.1 h]
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  have hab' := primeFactors_mono h hb0
  rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
  refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl
  exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
ha,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : φ 0 = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
a : ℕ
ha : ¬a = 0
hb : ¬a * 2 = 0
this : a.Coprime 2
⊢ a = a * 2 ∨ 2 * a = a * 2

Tactic:
· simp [mul_comm]

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

Goal state before:
pp: case neg
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a.Coprime c

Tactic:
refine coprime_of_dvd fun p hp hap ↦ ?_

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ i, (f i).lift g
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 c : α
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n, c - b = n • p

Tactic:
refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩
  · conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]
    rw [h, sub_smul]
    abel
  · rcases h with ⟨z, hz⟩
    rw [sub_eq_iff_eq_add] at hz
    rw [hz, toIcoMod_zsmul_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 : α
⊢ ∃ z, b = b + z • p

Tactic:
exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X → Prop
⊢ DenseRange Subtype.val ↔ Dense {x | p x}

Tactic:
by
  simp [DenseRange]

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 : α
⊢ toIocDiv hp a b = toIocDiv hp 0 (b - a)

Tactic:
by
  rw [toIocDiv_sub_eq_toIocDiv_add, zero_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' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

Tactic:
rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ 𝓝ˢ ∅ = ⊥

Tactic:
by rw [isOpen_empty.nhdsSet_eq, principal_empty]

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

Goal state before:
pp: case mp.mpr
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
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
H : p x ∈ U
⊢ p x ∈ g ⁻¹' q '' V

Tactic:
exact ⟨f x, e.ge H, congr_fun h.symm x⟩

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen[generateFrom g] s
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s

Tactic:
induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
C : Set α
⊢ IsClosed[t₂] C ↔ C = ∅ ∨ C = univ

Tactic:
simp [← isOpen_compl_iff, IndiscreteTopology.isOpen_iff, Or.comm]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a

Tactic:
exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
⊢ frontier (s ×ˢ univ) = frontier s ×ˢ univ

Tactic:
by
  simp [frontier_prod_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
⊢ frontier (univ ×ˢ s) = univ ×ˢ frontier s

Tactic:
by
  simp [frontier_prod_eq]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] s = 𝓟 s

Tactic:
by
  simp [nhdsSetWithin, principal_le_nhdsSet]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) ↔ Continuous[inst✝¹, inst✝] f

Tactic:
refine ⟨?_, fun hf ↦ hf.codRestrict hs⟩

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) → Continuous[inst✝¹, inst✝] f
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 '' o)

Tactic:
rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_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✝] (⋃ i, f '' ↑i)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
⊢ ContinuousOn (fun a ↦ f a b) sα

Tactic:
let g : α → γ := f.uncurry ∘ (fun a => (a, b))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ ContinuousOn (fun a ↦ f a b) sα
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ((fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i) ∧
    a i ∈ (fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i

pp: case refine_1.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) ⊆ s

Tactic:
· simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
      exact (h1 i).choose_spec.2

Goal state after:
case refine_1.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) ⊆ s
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:
classical
    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 refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
⊢ ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩

Goal state after:
case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (↑f ⊓ g).NeBot

Tactic:
rwa [inf_comm]

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g

Tactic:
refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩
  set g : Filter (sᶜ : Set α) := comap (↑) f
  have : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_ofPred])
  simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ t ≤ generateFrom (range (uncurry b))

pp: case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ generateFrom (range (uncurry b)) ≤ t

Tactic:
· rw [le_generateFrom_iff_subset_isOpen]
      rintro _ ⟨⟨x, n⟩, rfl⟩
      exact (hxb x n).right

Goal state after:
case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ generateFrom (range (uncurry b)) ≤ t
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

Tactic:
exact prod_mono (nhdsSet_mono ht) le_rfl hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)

Tactic:
by
  rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
  ext
  simp only [SetLike.mem_coe]
  simp [f.le_symm_apply]

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 = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
by
  suffices univ ∩ ⋂ i, (fun i : I ↦ s ↓∩ t i) i = ∅ 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
  simpa [Set.eq_empty_iff_forall_notMem, Subtype.forall] using hst

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
discreteTopology_subtype_iff

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ (∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)

Tactic:
by
  refine ⟨fun h _ ↦ ?_, fun h ↦ ?_⟩
  · exact subset_closure_inter_of_isPreirreducible_of_isOpen h
  · intro a b ha hb ⟨p, pS, pa⟩ bS
    by_contra! h0
    suffices p ∉ closure (S ∩ b) from this <| (h b hb bS) pS
    simp only [closure, mem_sInter, mem_ofPred_eq, and_imp, not_forall, exists_prop]
    use aᶜ
    grind [isClosed_compl_iff, subset_compl_iff_disjoint_left, disjoint_iff_inter_eq_empty]

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ ∀ (a b : X), a ≈ b → f a = f b

Tactic:
by
  change t2Setoid X ≤ Setoid.ker f
  exact sInf_le <| .of_injective_continuous
    (Setoid.kerLift_injective _) (hf.quotient_lift fun _ _ ↦ id)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
⊢ S.Infinite

Tactic:
intro hs

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
⊢ False
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
⊢ IsClosed[inst✝] (s ∩ a)

Tactic:
have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
⊢ IsClosed[inst✝] (s ∩ a)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ SeparatedNhds {f x} (f '' K \ interior s)

Tactic:
simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ LocallyConnectedSpace β

Tactic:
refine locallyConnectedSpace_iff_connectedComponentIn_open.2 fun F hF y _ ↦ ?_

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝] (connectedComponentIn F y)
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ i ∈ S, i ∈ l.curry m

Tactic:
exact hS

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty
    · exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩
    obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩
    · exact Or.inl ⟨t, ht.isPreconnected, rfl⟩
    · exact Or.inr ⟨t, ht.isPreconnected, rfl⟩

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
by
  constructor <;> intro h
  · induction h with
    | @basic s hs => exact ⟨{s}, by simp [hs]⟩
    | univ => exact ⟨∅, by simp⟩
    | superset _ _ ih => refine Exists.imp (fun S => ?_) ih; tauto
    | @sInter S Sct _ ih =>
      choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
      apply subset_sInter
      intro s H
      exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
  rcases h with ⟨S, Sg, Sct, hS⟩
  refine mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS
  intro s H
  exact CountableGenerateSets.basic (Sg H)

Goal state after: