mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
x y : (Discrete.functor F).ColimitType
h : (Discrete.functor F).descColimitType c x = (Discrete.functor F).descColimitType c y
⊢ x = y

Tactic:
obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
y : (Discrete.functor F).ColimitType
i : C
x : (Discrete.functor F).obj { as := i }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c y
⊢ (Discrete.functor F).ιColimitType { as := i } x = y
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
⊢ c.inj i₁ y₁ = c.inj i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ by subst h₁ h₂; rfl⟩
  obtain rfl := eq_of_inj_apply_eq_of_isColimit hc _ _ h
  exact ⟨rfl, (inj_injective_of_isColimit hc i₁ h).symm⟩

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

Goal state before:
pp: C : Type u
F : C → Type v
x✝ : Cocone (Functor.empty (Type u))
⊢ ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    ({ pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        ↾fun x ↦ PEmpty.elim x) =
      x✝.ι.app j

Tactic:
by rintro ⟨⟨⟩⟩

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

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝ =
    (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      x✝

Tactic:
apply Eq.symm

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      x✝ =
    (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

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

Tactic:
Set.range_comp _ Sum.inr,

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inr)ᶜ
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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' = ↑(extensionOfMax i f).toLinearPMap x

Tactic:
ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]),

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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x + (ExtensionOfMaxAdjoin.extendIdealTo i f h y) 0 =
    ↑(extensionOfMax i f).toLinearPMap x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
have : d ∣ b := by
      rw [← hb2]
      apply gcd_dvd_right

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case e'_2
n : ℕ
⊢ (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) = ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

Tactic:
rw [sum_eq_sum_Ico_succ_bot] <;> simp

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
x : α
hx : x ∈ ⋂ i, Ici ↑i
y : α
hy : x ≤ y
⊢ p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : n.factorization p ≠ 0
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
← zero_lt_iff

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
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
⊢ False

Tactic:
rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (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
Module: Mathlib.Data.Nat.Totient

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

Tactic:
by
  by_cases ha : a = 0
  · rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'
    simp [ha, h']
  by_cases hb : b = 0
  · rw [hb, totient_zero, totient_eq_zero] at h'
    exact False.elim (ha h')
  obtain ⟨c, rfl⟩ := h
  suffices a.Coprime c by
    rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]
  refine coprime_of_dvd fun p hp hap ↦ ?_
  rintro ⟨d, rfl⟩
  suffices a.totient < (p * a * d).totient by
    rw [← mul_assoc, mul_comm a] at h'
    exact h'.not_lt this
  rw [mul_comm p]
  refine lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))
  · 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
  · exact totient_pos.mpr <| zero_lt_of_ne_zero (by rwa [mul_assoc])

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

Tactic:
simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIcoDiv hp (-a) b • p + 1 • p) = p - (b - toIcoDiv hp (-a) b • p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ pure x ≤ F.lift' closure[inst✝]

Tactic:
(hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ {x} ⊆ closure[inst✝] (id i')
Module: Mathlib.Topology.Order

Goal state before:
pp: case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
hS : ∀ s ∈ S✝, a ∈ s → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 (⋃₀ S✝)

Tactic:
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

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
⊢ h.trans h.symm = Homeomorph.refl X

Tactic:
by
  ext
  apply symm_apply_apply

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

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

Tactic:
by
  rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.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:
by
    haveI := sInf tas; haveI := sInf tbs
    exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)

Tactic:
continuous_iff_continuousAt

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
refine Or.inl ⟨?_, ?_⟩

Goal state after:
case inr.mp.refine_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝¹] s

case inr.mp.refine_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝] t
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 : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)

Tactic:
rw [← disjoint_principal_right]

Goal state after:
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 : X
⊢ Disjoint (𝓝 (f x)) (𝓟 (range g))
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α

Tactic:
separableSpace_iff,

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ s, s.Countable ∧ Dense s
Module: Mathlib.Topology.Bases

Goal state before:
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_iff_nhds]
      intro x
      rw [(hbb x).ge_iff]
      intro n _
      refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left
      exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩

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, f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ n, L n) ∩ s

Tactic:
by rw [preimage_iUnion, iUnion_inter]

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

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

Tactic:
← 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
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace X

Tactic:
by
  refine compactSpace_generateFrom hT fun P hP𝔅 hP ↦ ?_
  contrapose! hP
  simp_rw [← Set.nonempty_compl, Set.compl_sUnion] at hP ⊢
  refine h _ ?_ fun Q hQP hQ ↦ ?_
  · rintro _ ⟨S, hS, rfl⟩
    exact h𝔅 _ (hP𝔅 hS)
  · replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
    exact hP hQP (hQ.image _)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x✝

Tactic:
rename_i x

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
    IsOpen s →
      (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) →
        ∀ x ∈ s, ∀ y ∈ s, ¬x = y → ∀ (U : Set X), IsOpen U → Xor (x ∈ U) (y ∈ U) → x ∈ U ∧ y ∉ U → False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ⊆ x
⊢ x ⊆ s

Tactic:
have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)

Goal state after:
case mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ⊆ x
this : closure[inst✝] x ⊆ s
⊢ x ⊆ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_3.htd
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := ⋯
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) fun i ↦ (↑i)ᶜ

Tactic:
rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → ¬ClusterPt x (𝓟 S)) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
clusterPt_iff_not_disjoint,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → ¬¬Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst✝] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst✝] (S ∩ U)
⊢ False

Tactic:
obtain ⟨x, h₁, h₂, h₃⟩ :=
    hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst✝] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst✝] (S ∩ U)
x : X
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ (closure[inst✝] (S ∩ U))ᶜ
⊢ False
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U

Tactic:
by
  rw [preirreducibleSpace_iff, isPreirreducible_iff_subset_closure_inter_open]
  simp only [univ_inter, univ_subset_iff, Dense]
  grind

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x

Tactic:
by
  rwa [ContinuousAt, eq_of_tendsto_nhds h]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ IsCompact (closure[inst✝¹] K)

Tactic:
refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hKU : closure[inst✝¹] K ⊆ ⋃ i, U i
⊢ ∃ t, closure[inst✝¹] K ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen[inst✝²] V ∧ K ⊆ V ∧ IsCompact (closure[inst✝²] V)

Tactic:
exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩

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

Goal state before:
pp: case refl
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (⋃ j ∈ {i}, s j)

Tactic:
rw [biUnion_singleton]

Goal state after:
case refl
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
⊢ ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

Tactic:
by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
z : α
hz : z ∈ u
t : α
ht : P z t ∧ P t z
⊢ t ∈ u

Tactic:
exact h'.trans x z t hz ht.1

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
      refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
      · simpa only [hsf, image_union] using image_mono (f := f) hsuv
      · simpa only [image_preimage_inter] using hsu.image f
      · simpa only [image_preimage_inter] using hsv.image f

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := ⋯
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint (⋂ i, t i)ᶜᶜ s

Tactic:
simp only [compl_iInter, compl_iUnion, compl_compl]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint (⋂ i, t i) s