mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
simp only [packingNumber, ENNReal.coe_mul, ENNReal.coe_ofNat, externalCoveringNumber, le_iInf_iff,
    iSup_le_iff]
  intro C hC_cover D hD_subset hD_separated
  -- For each point in D, choose a point in C which is ε-close to it
  let f : D → C := fun x ↦
    ⟨(hC_cover (hD_subset x.2)).choose, (hC_cover (hD_subset x.2)).choose_spec.1⟩
  have hf' (x : D) : edist x.1 (f x) ≤ ε := (hC_cover (hD_subset x.2)).choose_spec.2
  -- `⊢ D.encard ≤ C.encard`
  -- It suffices to prove that `f` is injective
  simp only [← Set.toENat_cardinalMk]
  gcongr
  refine Cardinal.mk_le_of_injective (f := f) fun x y hxy ↦ Subtype.ext ?_
  apply Set.Pairwise.eq hD_separated x.2 y.2
  simp only [not_lt]
  calc
    edist (x : X) y ≤ edist (x : X) (f x) + edist (f x : X) y := edist_triangle ..
    _ ≤ 2 * ε := by
      rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y

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

Goal state before:
pp: x✝ : ℕ
⊢ Continuous fun a ↦ cantorSpaceHomeomorphNatToCantorSpace a x✝

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → ↑KC := Subtype.coind f ⋯
hf'_surjective : Function.Surjective f'
h : ↑KC → ↑KH := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ Continuous (⇑g.symm ∘ h ∘ f')

Tactic:
by fun_prop

Goal state after:
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
s t : ℝ≥0
hf₁ : MemHolder r f
hf₂ : MemHolder t f
hrs : r ≤ s
hst : s ≤ t
⊢ MemHolder s f

Tactic:
by
  simp_rw [MemHolder, ← holderOnWith_univ] at *
  exact HolderOnWith.exists_holderOnWith_of_le_of_le hf₁ hf₂ hrs hst

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
constructor
  · intro h x₁ x₂
    by_cases hx : x₁ = x₂
    · rw [hx]
    · rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot] at h
      rw [← edist_eq_zero, ← nonpos_iff_eq_zero]
      refine le_of_forall_gt fun b hb => ?_
      obtain ⟨C, hC, hC'⟩ := h (b / edist x₁ x₂ ^ (r : ℝ))
        (ENNReal.div_pos hb.ne.symm (ENNReal.rpow_lt_top_of_nonneg zero_le_coe
          (edist_lt_top x₁ x₂).ne).ne)
      exact lt_of_le_of_lt (hC x₁ x₂) <| ENNReal.mul_lt_of_lt_div hC'
  · intro h
    rcases isEmpty_or_nonempty X with hX | hX
    · exact eHolderNorm_of_isEmpty
    · rw [← eHolderNorm_const X r (f hX.some)]
      congr
      simp [funext_iff, h _ hX.some]

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Tactic:
exact hC x₁ x₂

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
⊢ toGHSpace X = toGHSpace Y → Nonempty (X ≃ᵢ Y)

Tactic:
simp only [toGHSpace]
    rw [Quotient.eq]
    rintro ⟨e⟩
    have I :
      (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) =
        (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
    have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
    exact ⟨f.trans <| (cast I e).trans g⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lowerBasis α = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} → s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
rintro ⟨F, ⟨hF, hs⟩, rfl⟩
    have := hF.to_subtype
    rw [subset_def, Subtype.forall'] at hs
    choose f hf using hs
    exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsLowerSet α
inst✝ : IsLower α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_isLowerSet α _ t₁]
  exact IsLower.isLowerSet_of_isOpen hs

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

Goal state before:
pp: case mpr.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] univ

pp: case mpr.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen[inst✝¹] (Iic a)ᶜ

Tactic:
· exact isOpen_univ

Goal state after:
case mpr.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen[inst✝¹] (Iic a)ᶜ
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ L

Tactic:
rw [@IsLawson.topology_eq_lawson α _ L _]
  exact scottHausdorff_le_lawson

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

Goal state before:
pp: case refine_2.h₁
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ ((fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x}).Nonempty

Tactic:
exact Set.Nonempty.image _ <| Set.Nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩

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

Goal state before:
pp: X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) (range Subtype.val)

Tactic:
exact ghDist_le_hausdorffDist ha hb

Goal state after:
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case e'_5.inr.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)

Tactic:
cases hm

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
n : ℕ
⊢ Continuous[inst✝, _] fun x ↦ (f n) x * (1 / 2 / 2 ^ n)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
hV : p₀ ∈ unop V
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)

Tactic:
simp only [dif_pos hW, dif_pos hV, eqToHom_trans]

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ (((skyscraperPresheafCocone p₀ A y).ι.app U ≫ eqToHom ⋯) ≫
        ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE ⋯).op) ≫
      c.ι.app (op (h1.choose ⊓ unop U)) =
    ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE ⋯).op ≫ c.ι.app (op (h1.choose ⊓ unop U))

Tactic:
congr 1

Goal state after:
case e_a
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ ((skyscraperPresheafCocone p₀ A y).ι.app U ≫ eqToHom ⋯) ≫
      ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE ⋯).op =
    ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f = (eqToHom ⋯ ≫ (skyscraperPresheafCocone p₀ A y).ι.app (op h1.choose)) ≫ f

Tactic:
congr 1

Goal state after:
case e_a
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt = eqToHom ⋯ ≫ (skyscraperPresheafCocone p₀ A y).ι.app (op h1.choose)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ PUnit.unit ∉ ⊥

Tactic:
#adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1}

Goal state after:
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : Preorder X
inst✝² : Topology.IsUpperSet X
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimits C
F : X ⥤ C
α : Type v
Us : α → Opens X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
x y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
⊢ S.π.app ((projSup Us).obj x) ≫
      ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ((projSup Us).map e) ≫
        limit.π (generator (principalOpen y.right) ⋙ F)
          { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) } =
    S.π.app ((projSup Us).obj x) ≫
      limit.π (generator (principalOpen x.right) ⋙ F)
          { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } ≫
        F.map ((generator (iSup Us)).map e)

Tactic:
congr 1

Goal state after:
case e_a
X : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : Preorder X
inst✝² : Topology.IsUpperSet X
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimits C
F : X ⥤ C
α : Type v
Us : α → Opens X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
x y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
⊢ ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ((projSup Us).map e) ≫
      limit.π (generator (principalOpen y.right) ⋙ F)
        { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) } =
    limit.π (generator (principalOpen x.right) ⋙ F)
        { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } ≫
      F.map ((generator (iSup Us)).map e)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ S.π.app (Opposite.op VV) ≫
      ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ee.op ≫
        limit.π (generator (principalOpen x) ⋙ F)
          { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    S.π.app (Opposite.op { obj := V, property := ⋯ }) ≫
      limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
congr 1

Goal state after:
case e_a
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ee.op ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ Continuous fun s ↦ ⟨(↑s).base, ⋯⟩

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
g' : ↑(base ⁻¹' ↑U)
hgU : (↑g').base ∈ U
hgf : (↑g').germ = (ConcreteCategory.hom (F.germ U (↑g').base hgU)) f
⊢ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑g').germ)) =
    WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ g.germ))

Tactic:
congr 1

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
g' : ↑(base ⁻¹' ↑U)
hgU : (↑g').base ∈ U
hgf : (↑g').germ = (ConcreteCategory.hom (F.germ U (↑g').base hgU)) f
⊢ (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑g').germ) =
    (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ g.germ)
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
g' : ↑(base ⁻¹' ↑U)
hgU : (↑g').base ∈ U
hgf : (↑g').germ = (ConcreteCategory.hom (F.germ U (↑g').base hgU)) f
⊢ (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ ((ConcreteCategory.hom (F.germ U (↑g').base hgU)) f)) =
    (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ g.germ)

Tactic:
← hf,

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
g' : ↑(base ⁻¹' ↑U)
hgU : (↑g').base ∈ U
hgf : (↑g').germ = (ConcreteCategory.hom (F.germ U (↑g').base hgU)) f
⊢ (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ ((ConcreteCategory.hom (F.germ U (↑g').base hgU)) f)) =
    (ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ ((ConcreteCategory.hom (F.germ U g.base hg)) f))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
j✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op) =
    F.map ((leSupr U j✝.as.2).op ≫ ((U j✝.as.1).infLERight (U j✝.as.2)).op)

Tactic:
congr 1

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    f.hom ≫ (coneEquivInverseObj F U c').π.app j = (coneEquivInverseObj F U c).π.app j

Tactic:
intro x
        induction x with | op x => ?_
        rcases x with (⟨i⟩ | ⟨i, j⟩)
        · dsimp
          dsimp only [Fork.ι]
          rw [← f.w WalkingParallelPair.zero, Category.assoc]
        · dsimp
          rw [← f.w WalkingParallelPair.one, Category.assoc]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ IsCompact univ

Tactic:
rw [← range_quotient_mk']
  exact isCompact_range (continuous_sum_dom.2
    ⟨(isometry_optimalGHInjl X Y).continuous, (isometry_optimalGHInjr X Y).continuous⟩)

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (cocone U).op).π.app (op (single a✝)) =
    ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝))

Tactic:
simp
              rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 (Functor.mapCone F (cocone U).op).pt ≫
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝)) =
    (Functor.mapCone F (cocone U).op).π.app (op (single a✝))

Tactic:
simp
              rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ 𝟙 ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).pt ≫
      (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.zero =
    ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.zero

Tactic:
simp
              rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ 𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
      ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.zero =
    (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.zero

Tactic:
simp
              rfl

Goal state after: