mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case refine_1
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ IsOpen[inst✝] (some '' s')

pp: case refine_2
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ Subtype.val ⁻¹' some '' s' = Subtype.val ⁻¹' Metric.eball (some x) r

Tactic:
· exact (IsOpenEmbedding.isOpen_iff_image_isOpen h).mp s'o

Goal state after:
case refine_2
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ Subtype.val ⁻¹' some '' s' = Subtype.val ⁻¹' Metric.eball (some x) r
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
exact ⟨i, iH⟩

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

Goal state before:
pp: case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
exact ⟨i, iH⟩

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
· rw [isProperMap_iff_ultrafilter]
    refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
    have := H.2 F isClosed_closure
    have : (y, 𝒰) ∈ Prod.map f id '' F :=
      this.mem_of_tendsto (hy.prodMk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
    rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
    refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
    rw [mem_closure_iff_nhds] at hx
    rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc))
      with ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
    exact hy' hy

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius + 1 - 1 = ↑(logSizeBallSeq J hJ a c l).radius

pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ ↑(logSizeBallSeq J hJ a c l).radius

Tactic:
ENNReal.add_sub_cancel_right (ENNReal.one_ne_top)

Goal state after:
case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius = ↑(logSizeBallSeq J hJ a c l).radius

T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ ↑(logSizeBallSeq J hJ a c l).radius
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
n : ℕ
inst✝ : MetricSpace α
x : ℕ → α
a : α
⊢ (fun n ↦ dist a (x n) - dist (x 0) (x n)) ∈ lp (fun x ↦ ℝ) ∞

Tactic:
by
    apply memℓp_infty
    use dist a (x 0)
    rintro - ⟨n, rfl⟩
    exact abs_dist_sub_le _ _ _

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

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
apply Sum.one_le_dist_inl_inr

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

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
apply Sum.one_le_dist_inl_inr

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

Goal state before:
pp: case refine_1
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_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ (f '' C).encard ≤ C.encard

Tactic:
exact encard_image_le f C

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep.toReal = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
ENNReal.toReal_eq_zero_iff

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ∨ s.einfsep = ∞ ↔ s.einfsep = 0 ∨ s.einfsep = ∞
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ

Tactic:
compl_Ici,

Goal state after:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ

Tactic:
compl_Ici,

Goal state after:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ Iio (min b c) = Iio b ∩ (Ici c)ᶜ
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ Iio (min b c) = Iio b ∩ (Ici c)ᶜ

Tactic:
compl_Ici,

Goal state after:
case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
b c : α
⊢ Iio (min b c) = Iio b ∩ Iio c
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
D : Set (Set α)
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
inst✝ : IsScott α D
hf : Continuous[inst✝⁴, inst✝²] f
x✝ b : α
hab : x✝ ≤ b
h : ¬f x✝ ≤ f b
⊢ False

Tactic:
simpa only [mem_compl_iff, mem_preimage, mem_Iic, le_refl, not_true]
    using isUpperSet_of_isOpen (D := D) ((isOpen_compl_iff.2 isClosed_Iic).preimage hf) hab h

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

Goal state before:
pp: case inl
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : X
⊢ f (inl val✝) ∈ range Φ ∪ range Ψ

pp: case inr
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : Y
⊢ f (inr val✝) ∈ range Φ ∪ range Ψ

Tactic:
· apply mem_union_left; apply mem_range_self

Goal state after:
case inr
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : Y
⊢ f (inr val✝) ∈ range Φ ∪ range Ψ
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
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt ⟶ c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι.app j ≫ f = c.ι.app j
⊢ f = eqToHom ⋯ ≫ c.ι.app (op ⊤)

Tactic:
dsimp
    rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
      Category.id_comp]

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

Goal state before:
pp: case refine_2
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x : q.Rep), ∃ y, dist x (Φ y) ≤ ε

Tactic:
show ∀ x : q.Rep, ∃ z : s p, dist x (Φ z) ≤ ε
      -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
      intro x
      have : x ∈ ⋃ y ∈ s q, ball y ε := (hs q).2 (mem_univ _)
      obtain ⟨y, ys, hy⟩ := mem_iUnion₂.1 this
      let i : ℕ := E q ⟨y, ys⟩
      let hi := ((E q) ⟨y, ys⟩).is_lt
      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
      have hiq : i < N q := hi
      have hip : i < N p := by rwa [Npq.symm] at hiq
      let z := (E p).symm ⟨i, hip⟩
      use z
      have C1 : (E p) z = ⟨i, hip⟩ := (E p).apply_symm_apply ⟨i, hip⟩
      have C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl
      have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ := by
        rw [ihi_eq]; exact (E q).symm_apply_apply ⟨y, ys⟩
      have : Φ z = y := by simp only [Φ, Ψ]; rw [C1, C2, C3]
      rw [this]
      exact hy.le

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ (ConcreteCategory.hom (T.app (op W))) ((ConcreteCategory.hom (ℱ.map hWV.op)) s) =
    (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s)

Tactic:
simp only [← ConcreteCategory.comp_apply, T.naturality]

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

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
⊢ dist x y ≤ C

Tactic:
change dist (x : p.Rep) y ≤ C

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
⊢ dist ↑x ↑y ≤ C
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
y : Y
⊢ BddBelow (range fun x ↦ g (inl x, inr y))

Tactic:
change BddBelow (range fun x : X => g (inl x, inr y))

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
y : Y
⊢ BddBelow (range fun x ↦ g (inl x, inr y))
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.stalkToFiber x))

Tactic:
apply TopCat.stalkToFiber_surjective

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : F.stalk x), ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
⊢ hZ_irred.genericPoint ∈ ⋂₀ B

Tactic:
rw [Set.mem_sInter]

Goal state after:
case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
⊢ ∀ t ∈ B, hZ_irred.genericPoint ∈ t
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
⊢ False

Tactic:
let J1 := setOfPred_sublevelLeft_subset X Y f t t' y1 y2

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
⊢ False