mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
H : FiniteIndexNormalSubgroup ↑G
⊢ FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id ↑G) ⋯) =
    𝟙 (FiniteGrp.of (↑G ⧸ H.toSubgroup))

Tactic:
ext ⟨x⟩

Goal state after:
case mk
G : GrpCat
H : FiniteIndexNormalSubgroup ↑G
x✝ : ↑(FiniteGrp.of (↑G ⧸ H.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x) =
    (ConcreteCategory.hom (𝟙 (FiniteGrp.of (↑G ⧸ H.toSubgroup)))) (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
X✝ Y✝ Z✝ : FiniteIndexNormalSubgroup ↑G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯) =
    FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Y✝.toSubgroup (MonoidHom.id ↑G) ⋯) ≫
      FiniteGrp.ofHom (QuotientGroup.map Y✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)

Tactic:
ext ⟨x⟩

Goal state after:
case mk
G : GrpCat
X✝ Y✝ Z✝ : FiniteIndexNormalSubgroup ↑G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(FiniteGrp.of (↑G ⧸ X✝.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x) =
    (ConcreteCategory.hom
        (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Y✝.toSubgroup (MonoidHom.id ↑G) ⋯) ≫
          FiniteGrp.ofHom (QuotientGroup.map Y✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : xs₀ ~ map Sigma.snd xs
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁

Tactic:
h₁

Goal state after:
case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : xs₀ ~ xs₁
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ Tendsto (⇑φ.symm ∘ F) ℱ (𝓝 (φ.symm f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
φ.symm.isInducing.tendsto_nhds_iff

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ Tendsto (⇑φ.symm ∘ F) ℱ (𝓝 (φ.symm f)) ↔ Tendsto (⇑φ.symm ∘ F) ℱ (𝓝 (φ.symm f))
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case 𝔖_covers
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ⋃₀ {K | IsCompact K} = univ

Tactic:
exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: M : Type u_1
inst✝³ : GroupWithZero M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousInv₀ M
inst✝ : T1Space M
⊢ IsOpenEmbedding Units.val

Tactic:
by
    refine ⟨Units.isEmbedding_val₀, ?_⟩
    convert! (isClosed_singleton (X := M) (x := 0)).isOpen_compl
    ext
    simp only [Set.mem_range, Set.mem_compl_iff, Set.mem_singleton_iff]
    exact isUnit_iff_ne_zero

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace R
inst✝² : T2Space R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
I : Ideal R
⊢ IsOpen ↑I ↔ Finite (R ⧸ I)

Tactic:
by
  refine ⟨AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup, fun H ↦ ?_⟩
  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I
  exact AddSubgroup.isOpen_mono (H₁ := (maximalIdeal R ^ n).toAddSubgroup)
    (H₂ := I.toAddSubgroup) hn (isOpen_maximalIdeal_pow R n)

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ derivedSet U ⊆ derivedSet a ∪ derivedSet b

Tactic:
← derivedSet_union

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ derivedSet U ⊆ derivedSet (a ∪ b)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst✝ : IsGeneratedBy X Y
U : Set Y
⊢ IsClosed[tY] U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed[inst✝¹ i] (⇑f ⁻¹' U)

Tactic:
simp [← (homeomorph (X := X)).isQuotientMap.isClosed_preimage,
    WithGeneratedByTopology.isClosed_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ SequentialSpace X

Tactic:
exact SequentialSpace.iSup (fun n ↦ SequentialSpace.iSup
    (fun f ↦ SequentialSpace.coinduced _))

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), ↑F ⊆ T1 → (⋂₀ ι F).Nonempty
⊢ X.str F = x

Tactic:
obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : J i
⊢ ↑a i = ↑b i

Tactic:
exact congr_fun h ⟨i, hi⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

pp: case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i

Tactic:
· apply continuous_bot

Goal state after:
case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h✝ : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
j : cell C n
h : Disjoint A (openCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

pp: case inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h✝ : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
j : cell C n
h : IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
· left
    rw [disjoint_iff_inter_eq_empty.1 h]
    exact isClosed_empty

Goal state after:
case inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h✝ : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
j : cell C n
h : IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case inr
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
⊢ (⋂ i, s i).Nonempty

Tactic:
by_cases! h₀ : ∀ n, s n ∉ S

Goal state after:
case pos
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∀ (n : ℕ), s n ∉ S
⊢ (⋂ i, s i).Nonempty

case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
⊢ (⋂ i, s i).Nonempty
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ (πs C o) (Products.eval (π C fun x ↦ ord I x < o) ↑q) ∈ Products.eval C '' {m | m < ↑l}

Tactic:
rw [Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)]

Goal state after:
case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ Products.eval C ↑q ∈ Products.eval C '' {m | m < ↑l}
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U

Tactic:
have h : b ∈ Icc a c := ⟨Fact.out, Fact.out⟩

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
let f := hB.natEmbedding

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
⊢ ∃ a ∈ A, AccPt a (𝓟 B)
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g

Tactic:
rw [continuousGeneratedBy_def]
    intro i f
    exact (h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
l : Filter X
⊢ Tendsto pure l (𝓝 l)

Tactic:
rw [Filter.tendsto_nhds]

Goal state after:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
⊢ 0 ∈ preCantorSet n

Tactic:
by
  induction n with
  | zero =>
    simp [preCantorSet]
  | succ n ih =>
    exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
⊢ transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

Tactic:
by
  ext; simp_rw [transAt, coe_copy, Function.update_apply, if_neg h, if_neg h.symm]
  split_ifs <;>
    · congr 1; ext1; simp only [Function.update, eq_rec_constant, dite_eq_ite]
      apply ite_ite_comm; rintro rfl; exact h.symm

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ C'.encard ≤ (f '' C').encard

Tactic:
InjOn.encard_image

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ C'.encard ≤ C'.encard

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ InjOn f C'
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = ∞ ↔ ¬eHolderNorm r f ≠ ∞

Tactic:
not_not

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = ∞ ↔ eHolderNorm r f = ∞
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
by_cases hfg : MemHolder r f ∧ MemHolder r g

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : ¬(MemHolder r f ∧ MemHolder r g)
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ENNReal.ofReal d ≤ ENNReal.ofReal (dist x y)) ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
ENNReal.ofReal_le_ofReal_iff dist_nonneg

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ IsometryRel.setoid (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y) →
    Nonempty (X ≃ᵢ Y)

Tactic:
rintro ⟨e⟩

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ Nonempty (X ≃ᵢ Y)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ Nonempty (X ≃ᵢ Y) → toGHSpace X = toGHSpace Y

Tactic:
rintro ⟨e⟩

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
⊢ toGHSpace X = toGHSpace Y
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧

Tactic:
have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ ⟦p⟧ = toGHSpace X →
    ⟦q⟧ = toGHSpace Y →
      hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
        hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
hp

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
⊢ ⟦q⟧ = toGHSpace Y →
    hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
      hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
⊢ ∃ y ∈ range Ψ, dist (Φ xX) y < diam univ + 1 + diam univ

Tactic:
rw [Ψrange]

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
⊢ ∃ y ∈ ↑q, dist (Φ xX) y < diam univ + 1 + diam univ
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
  exact h.isClosed_biUnion fun _ _ => isClosed_Ici

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
rw [topology_eq α D]

Goal state after:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[scott α D] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: h : Set Prop
hs : h ∈ {Ioi True, {True}}
⊢ ∃ a, Ioi a = h

Tactic:
← Ioi_False

Goal state after:
h : Set Prop
hs : h ∈ {Ioi True, Ioi False}
⊢ ∃ a, Ioi a = h