mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
have h_mem := cantorSequence_mem_cantorSet hx n

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (cantorSequence x).get n ∈ cantorSet
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ Set.Icc 0 1
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
simp only [Set.mem_Icc] at h_mem

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

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

Tactic:
by
  constructor <;> intro H
  -- The direct implication is clear.
  · exact ⟨H.continuous, H.universally_closed _⟩
  · rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
    refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
  -- In `X × Filter X`, consider the closed set `F := closure {(x, ℱ) | ℱ = pure x}`
    let F : Set (X × Filter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
  -- Since `f × id` is closed, the set `(f × id) '' F` is also closed.
    have := H.2 F isClosed_closure
  -- Let us show that `(y, 𝒰) ∈ (f × id) '' F`.
    have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
  -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
  -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
  -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
  -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.
      this.mem_of_tendsto (hy.prodMk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
  -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.
    rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
  -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
  -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is an ultrafilter,
  -- it is enough to show that `Uᶜ` is not in `𝒰`.
    refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
    rw [mem_closure_iff_nhds] at hx
  -- Indeed, if that was the case, the set `V := {𝒢 : Filter X | Uᶜ ∈ 𝒢}` would be a neighborhood
  -- of `𝒰` in `Filter X`, hence `U ×ˢ V` would be a neighborhood of `(x, 𝒰) : X × Filter X`.
  -- But recall that `(x, 𝒰) ∈ F = closure {(x, ℱ) | ℱ = pure x}`, so the neighborhood `U ×ˢ V`
  -- must contain some element of the form `(z, pure z)`. In other words, we have `z ∈ U` and
  -- `Uᶜ ∈ pure z`, which means `z ∈ Uᶜ` by the definition of pure.
  -- This is a contradiction, which completes the proof.
    rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOfPred_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
    exact hz' hz

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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A

Tactic:
← encard_maximalSeparatedSet h_top

Goal state after:
case pos
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ (maximalSeparatedSet ε A).encard
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
⊢ ⨅ (_ : f '' C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
simp only [Set.image_subset_iff]

Goal state after:
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
⊢ ⨅ (_ : C ⊆ f ⁻¹' f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
by
  simp_rw [le_einfsep_iff, forall_mem_image]

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : x ∈ univ.pi s
y : (i : β) → X i
hy : y ∈ univ.pi s
hxy : x ≠ y
⊢ c ≤ edist x y

Tactic:
mem_univ_pi

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → X i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r ↦ 0 < r ∧ r < R x) fun r ↦ ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ a, ball (c a) (r' a)
hfin : LocallyFinite fun a ↦ ball (c a) (r' a)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs
      (fun x _ => hfin.point_finite x) hsub' with
    ⟨r, hsub, hlt⟩

Goal state after:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r ↦ 0 < r ∧ r < R x) fun r ↦ ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ a, ball (c a) (r' a)
hfin : LocallyFinite fun a ↦ ball (c a) (r' a)
r : ι → ℝ
hsub : s ⊆ ⋃ i, ball (c i) (r i)
hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
H : (𝓤 X).HasBasis (fun x ↦ 0 < x) fun x ↦ {p | edist p.1 p.2 < x ^ α⁻¹}
⊢ 𝓤 (Snowflaking X α hα₀ hα₁) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp (disch := positivity) [uniformity_comap, H.eq_biInf, ENNReal.rpow_lt_rpow_iff]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' closedEBall x r ↔ { val := y } ∈ closedEBall (toSnowflaking x) (r ^ α)

Tactic:
simp (disch := positivity) [ENNReal.rpow_le_rpow_iff]

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

Goal state before:
pp: case refine_1
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x✝¹ x✝ : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
a✝¹ : ⟦x✝¹⟧ = toGHSpace X
a✝ : ⟦x✝⟧ = toGHSpace Y
ht : hausdorffDist ↑x✝¹ ↑x✝ = t
⊢ 0 ≤ t

Tactic:
← ht

Goal state after:
case refine_1
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x✝¹ x✝ : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
a✝¹ : ⟦x✝¹⟧ = toGHSpace X
a✝ : ⟦x✝⟧ = toGHSpace Y
ht : hausdorffDist ↑x✝¹ ↑x✝ = t
⊢ 0 ≤ hausdorffDist ↑x✝¹ ↑x✝
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
h :
  ∀ t ∈ s,
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
x✝ : a ∈ ⋃₀ s
s₀ : Set α
hs₀s : s₀ ∈ s
has₀ : a ∈ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
obtain ⟨b, hbd, hbds₀⟩ := h s₀ hs₀s hd₀ hd₁ hd₂ hd₃ has₀
    exact ⟨b, hbd, Set.subset_sUnion_of_subset s s₀ hbds₀ hs₀s⟩

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

Goal state before:
pp: case left
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ⊆ hull T (kernel S)

pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
· exact fun ⦃a⦄ a ↦ a (hull T (kernel S)) ⟨(isClosed_iff hT).mpr ⟨kernel S, rfl⟩,
      image_subset_iff.mp (fun _ hbS => sInf_le hbS)⟩

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ∀ t' ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}, hull T (kernel S) ⊆ t'

Tactic:
intro R

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set ↑T
⊢ R ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} → hull T (kernel S) ⊆ R
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
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
refine ⟨Φ, Ψ, ?_, ?_, ?_⟩

Goal state after:
case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Φ

case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Ψ

case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case inl
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₂
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

pp: case inr
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₃
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
· exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.left, hx⟩⟩

Goal state after:
case inr
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₃
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ leftRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom =
    (Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ leftRes G U

Tactic:
refine Pi.hom_ext _ _ fun b ↦ ?_

Goal state after:
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
b : ι × ι
⊢ (leftRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b =
    ((Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ leftRes G U) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ rightRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom =
    (Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ rightRes G U

Tactic:
refine Pi.hom_ext _ _ fun b ↦ ?_

Goal state after:
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
b : ι × ι
⊢ (rightRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b =
    ((Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ rightRes G U) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ autoParam (α.hom.app (op (iSup U)) ≫ Fork.ι ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)) = res F U)
    Fork.ext._auto_1

Tactic:
refine Pi.hom_ext _ _ fun b ↦ ?_

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
b : ι
⊢ (α.hom.app (op (iSup U)) ≫ Fork.ι ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U))) ≫
      Pi.π (fun i ↦ F.obj (op (U i))) b =
    res F U ≫ Pi.π (fun i ↦ F.obj (op (U i))) b
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝² : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝¹ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this✝ : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
t₆ : Under S.g s :=
  StructuredArrow.mk
    (CategoryOfElements.homMk ⟨op U, s⟩
      ((NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).obj
        ⟨op (iSup f), t₅⟩)
      (homOfLE le).op ⋯)
this : Nonempty (t₆ ⟶ t)
⊢ x ∈ unop (StructuredArrow.right t).fst

Tactic:
exact leOfHom ((ht t₆) this).some.right.1.unop ((le_iSup f 1) hW)

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: 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
this : (⋂₀ B).Nonempty
⊢ False

Tactic:
by simp_all [hB.prop.2.2]

Goal state after: