mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})

Tactic:
refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)

Goal state after:
case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (eval C) = Set.range (eval C ∘ ⇑(sum_equiv C hsC ho))

Tactic:
EquivLike.range_comp (e := sum_equiv C hsC ho)

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (eval C) = Set.range (eval C)
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
⊢ ∑ i, 1 ≤ ∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard

Tactic:
finsum_eq_sum_of_fintype

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
⊢ ∑ i, 1 ≤ ∑ i, (U i ∩ f ⁻¹' {y}).encard
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) (eval (π C fun x ↦ ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.subset_span

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
⊢ (πs C o) (eval (π C fun x ↦ ord I x < o) q) ∈ Products.eval C '' {m | m < ↑l}
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 : Products I
hq : m q ≠ 0
⊢ (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.subset_span

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 : Products I
hq : m q ≠ 0
⊢ (List.map (e C) (term I ho :: ↑q)).prod ∈ Products.eval C '' {m | m < ↑l}
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃₀ S)

Tactic:
by
  rw [sUnion_eq_biUnion]; exact hf.isCountablyCompact_biUnion hc

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
rw [isOpen_iff_mem_nhds]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

pp: t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
· linarith

Goal state after:
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
⊢ ↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Tactic:
by
  simp only [qRight, coe_zero, add_zero, div_one]
  split_ifs
  · rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]
    refine ⟨t.2.1, ?_⟩
    tauto
  · rw [(Set.projIcc_eq_right _).2]
    · linarith
    · exact zero_lt_one

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ ∀ (x : X × Y) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
· intro (x, y) (Ux, Uy) ⟨hUx, hUy⟩
    have : ContractibleSpace Ux := hUx.2
    have : ContractibleSpace Uy := hUy.2
    exact (Homeomorph.Set.prod Ux Uy).contractibleSpace

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
clear as hs

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
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)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (nhds (f x))
hx : ∀ t ∈ nhds (x, 𝒰.1), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Uᶜ ∈ pure z
⊢ False

Tactic:
exact hz' hz

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ infEDist p.1 ↑p.2

Tactic:
refine continuous_of_le_add_edist 2 (by simp) ?_

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
⊢ ∀ (x y : α × Closeds α), infEDist x.1 ↑x.2 ≤ infEDist y.1 ↑y.2 + 2 * edist x y
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖swap g a₀ i‖ ≤ ‖f a₀‖

Tactic:
← hgeq i ha₀_in_s

Goal state after:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖↑(f a₀) i‖ ≤ ‖f a₀‖
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ LipschitzWith (2 * maxVar X Y) f

Tactic:
apply LipschitzWith.of_dist_le_mul

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * maxVar X Y) * dist x y
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p ↦ infDist p.1 ↑p.2

Tactic:
rw [← one_add_one_eq_two]

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
⊢ LipschitzWith (1 + 1) fun p ↦ infDist p.1 ↑p.2
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: 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
⊢ coveringNumber ε (f '' A) = coveringNumber ε A

Tactic:
by
  refine le_antisymm ?_ ?_
  · simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    refine (iInf_le _ (C.image f)).trans ?_
    simp only [Set.image_subset_iff]
    have : ↑C ⊆ f ⁻¹' f '' A := hC_subset.trans (Set.subset_preimage_image f A)
    refine (iInf_le _ this).trans ?_
    rw [hf.isCover_image_iff]
    refine (iInf_le _ hC_cover).trans ?_
    exact encard_image_le f C
  · simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    obtain ⟨C', hC'_subset, rfl⟩ : ∃ C', C' ⊆ A ∧ C = C'.image f := by
      have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
      choose g hg_mem hg using this
      refine ⟨Set.range g, ?_, ?_⟩
      · rwa [Set.range_subset_iff]
      · ext
        simp
        grind
    refine (iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_
    simp only [hf.isCover_image_iff] at hC_cover
    refine (iInf_le _ hC_cover).trans ?_
    rw [InjOn.encard_image]
    exact hf_inj.mono hC'_subset

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep

Tactic:
by cases o <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ ∀ (i : ↑s.offDiag), x✝ ≤ uncurry edist ↑i

Tactic:
SetCoe.forall,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ ∀ x ∈ s.offDiag, x✝ ≤ uncurry edist x
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ edist (toSnowflaking x✝¹) (toSnowflaking x✝) = ENNReal.ofReal (dist (toSnowflaking x✝¹) (toSnowflaking x✝))

Tactic:
edist_toSnowflaking_toSnowflaking,

Goal state after:
case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ edist x✝¹ x✝ ^ α = ENNReal.ofReal (dist (toSnowflaking x✝¹) (toSnowflaking x✝))
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' ball x r = ball (toSnowflaking x) (r ^ α)

Tactic:
preimage_ofSnowflaking_ball x hr

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ball (toSnowflaking x) (r ^ α) = ball (toSnowflaking x) (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
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 : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤ diam univ + (diam univ + 1 + diam univ) + diam univ

Tactic:
rw [DΦ, DΨ]

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 : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam univ + dist (Φ xX) (Ψ z) + diam univ ≤ diam univ + (diam univ + 1 + diam univ) + diam univ
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝ : TopologicalSpace (α × β) := lower (α × β)
⊢ IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)

Tactic:
refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
a : α
x✝ : a ∈ s
⊢ IsOpen[lower (α × β)] (Prod.fst ⁻¹' Ici a)ᶜ

case refine_2.refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
b : β
x✝ : b ∈ t
⊢ IsOpen[lower (α × β)] (Prod.snd ⁻¹' Ici b)ᶜ
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : FunLike F α β
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ f b = ⊤
⊢ f ⊤ = ⊤

Tactic:
← top_le_iff.1 h.1,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : FunLike F α β
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ f b = ⊤
⊢ f b = ⊤
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed (s ∩ t)

Tactic:
← Subtype.image_preimage_val

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed (Subtype.val '' Subtype.val ⁻¹' t)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
δ : ℝ
δ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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have i' : i = (E q) (Ψ x) := by simp only [i, Ψ, Equiv.apply_symm_apply, Fin.val_cast]

Goal state after:
case refine_3
δ : ℝ
δ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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
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_1 Y : StructuredArrow (Opposite.op (iSup Us)) (principals X)⦄ (f : X_1 ⟶ Y),
    ((Functor.const (StructuredArrow (Opposite.op (iSup Us)) (principals X))).obj S.pt).map f ≫
        S.π.app ((projSup Us).obj Y) ≫
          limit.π (generator (principalOpen Y.right) ⋙ F)
            { left := { as := PUnit.unit }, right := Y.right,
              hom := 𝟙 ((fromPUnit (Opposite.op (principalOpen Y.right))).obj { as := PUnit.unit }) } =
      (S.π.app ((projSup Us).obj X_1) ≫
          limit.π (generator (principalOpen X_1.right) ⋙ F)
            { left := { as := PUnit.unit }, right := X_1.right,
              hom := 𝟙 ((fromPUnit (Opposite.op (principalOpen X_1.right))).obj { as := PUnit.unit }) }) ≫
        (generator (iSup Us) ⋙ F).map f

Tactic:
rintro x y e
      simp only [Functor.const_obj_obj, Functor.comp_obj, Functor.const_obj_map,
        Functor.op_obj, Functor.pointwiseRightKanExtension_obj,
        Category.id_comp, Functor.comp_map, Category.assoc]
      rw [← S.w ((projSup Us).map e), Category.assoc]
      congr 1
      let xx : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
        ⟨.mk .unit, x.right, 𝟙 _⟩
      let yy : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
        ⟨.mk .unit, y.right, .op <| LE.le.hom <| principalOpen_le e.right.le⟩
      let ee : xx ⟶ yy := { left := 𝟙 _, right := e.right }
      exact (limit.lift_π _ _).trans (limit.w
        (StructuredArrow.proj _ (principals X) ⋙ F) ee).symm

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

Goal state before:
pp: case refine_1
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₁

Tactic:
h₁,

Goal state after:
case refine_1
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₂ ⊓ sq.X₃
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
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
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε

Tactic:
have i' : i = (E q) (Ψ x) := by simp only [i, Ψ, Equiv.apply_symm_apply, Fin.val_cast]

Goal state after:
case refine_3
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))
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε