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')

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

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)

Tactic:
simpa using isOpen_Iio

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (cantorSequence x).get n ∈ cantorSet
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x

Tactic:
rw [cantorSequence_eq_self_sub_sum_cantorToTernary x n] at h_mem

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

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

Tactic:
rw [cantorSequence_eq_self_sub_sum_cantorToTernary x n] at h_mem

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ 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
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) Filter.atTop (nhds x)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le (g := fun n ↦ x - (3⁻¹ : ℝ) ^ n) (h := fun _ ↦ x)

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ x - 3⁻¹ ^ n) Filter.atTop (nhds x)

case hh
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x_1 ↦ x) Filter.atTop (nhds x)

case hgf
x : ℝ
hx : x ∈ cantorSet
⊢ (fun n ↦ x - 3⁻¹ ^ n) ≤ fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i

case hfh
x : ℝ
hx : x ∈ cantorSet
⊢ (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) ≤ fun x_1 ↦ x
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
have : 𝓝 (a::l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1::p.2 := by
    simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
      (Filter.seq_eq_filter_seq _ _).symm]
    simp [-Filter.map_def, Function.comp_def, functor_norm]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i f)) (2 * ↑(x✝ i))) fun j ↦ x✝ ↑j) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))

Tactic:
change f _ = _

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ f (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i)), fun j ↦ x✝ ↑j)) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inl.inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]

Goal state after:
case inl.inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
x₀ : T
hJ_card : ↑(#{x₀}) ≤ a ^ n
hJ : Nonempty ↥{x₀}
⊢ ∃ K ⊆ {x₀} ×ˢ {x₀},
    ↑(#K) ≤ a * ↑(#{x₀}) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
this : ↑s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t

Tactic:
t.isCompact.isClosed.closure_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
this : ↑s = ↑t
⊢ ↑s = ↑t
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this : ↑s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t

Tactic:
t.isCompact.isClosed.closure_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this : ↑s = ↑t
⊢ ↑s = ↑t
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
c : Y
⊢ ↑(nnHolderNorm r (Function.const X c)) ≤ eHolderNorm r (Function.const X c)

Tactic:
exact coe_nnHolderNorm_le_eHolderNorm

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

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

Tactic:
einfsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ d ≤ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

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

Tactic:
einfsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
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:
einfsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
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:
einfsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
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:
einfsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / ↑‖c‖₊

Tactic:
· rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div hc]
      refine HolderWith.eHolderNorm_le fun x₁ x₂ => ?_
      rw [coe_div hc, ← ENNReal.mul_div_right_comm,
        ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top,
        mul_comm, ← smul_eq_mul, ← ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply,
        ← Pi.smul_apply]
      exact hf.smul.holderWith 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
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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
⊢ ⨅ x, Fb (inl x, inr y) ≤ r

Tactic:
have : f (inr y) ∈ (q : Set _) := Ψrange ▸ (mem_range_self _)

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
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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this : f (inr y) ∈ ↑q
⊢ ⨅ x, Fb (inl x, inr y) ≤ r
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 _]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ lawson α
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
by
        refine hausdorffDist_triangle <| hausdorffEDist_ne_top_of_nonempty_of_bounded
          (range_nonempty _) (range_nonempty _) ?_ ?_
        · exact (isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y)))).isBounded
        · exact (isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjr X Y)))).isBounded

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

Goal state before:
pp: case neg
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
simp only [skyscraperPresheafStalkOfSpecializes, colimit.isoColimitCocone_ι_hom,
        skyscraperPresheafCoconeOfSpecializes_pt, skyscraperPresheafCoconeOfSpecializes_ι_app,
        Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, Functor.const_obj_obj]
      rw [comp_eqToHom_iff]
      apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

Goal state after:
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
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ := by
        have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2
        rw [Fin.heq_fun₂_iff Npq Npq] at hpq'
        rw [← hpq']

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))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
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✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
⊢ ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

Tactic:
have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) :=
      ciInf_le (by simpa using HD_below_aux2 0) default
    have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    exact le_trans A B

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

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
⊢ ∀ x ∈ range (optimalGHInjr X Y), ∃ y ∈ range (optimalGHInjl X Y), dist x y ≤ r

Tactic:
· rintro _ ⟨z, rfl⟩
    have I1 : (⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y)) < r :=
      lt_of_le_of_lt (le_max_right _ _) hr
    have I2 :
        ⨅ x, optimalGHDist X Y (inl x, inr z) ≤ ⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y) :=
      le_csSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _)
    have I : ⨅ x, optimalGHDist X Y (inl x, inr z) < r := lt_of_le_of_lt I2 I1
    rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩
    refine ⟨optimalGHInjl X Y z', mem_range_self _, le_of_lt ?_⟩
    rwa [dist_comm]

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

Goal state before:
pp: case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Tactic:
fconstructor

Goal state after:
case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ (y : ↥↑⟨U, m⟩) → F.stalk ↑y

case h.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ (_ : (Sheafify.isLocallyGerm F).pred ?h.w), ?h.w ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s
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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
⊢ x ∈ sublevelLeft X f b ↑y ∪ sublevelLeft X f b ↑y'

Tactic:
simp only [Set.mem_union, mem_sublevelLeft_iff, ← inf_le_iff]

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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_2
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)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ

Tactic:
calc
    dist p q = ghDist p.Rep q.Rep := dist_ghDist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ / 2 := by simp only [ε, one_div]; ring
    _ < δ := half_lt_self δpos

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x✝ : ↑I
⊢ ((γ.subpath t₀ (Icc.convexComb t₁ t₂ (1, x✝).1)).trans (γ.subpath (Icc.convexComb t₁ t₂ (1, x✝).1) t₂)) (1, x✝).2 =
    ((γ.subpath t₀ t₂).trans (Path.refl (γ t₂))).toContinuousMap x✝

Tactic:
by rw [Icc.convexComb_one, subpath_self, coe_toContinuousMap]

Goal state after:
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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
have hmax_y (x) (hx : x ∈ X) : ∃ y ∈ Y, IsMaxOn (f x) Y y := (hfx x hx).exists_isMaxOn ne_Y kY
  choose! η η_mem η_max using hmax_y
  have hlsc : LowerSemicontinuousOn (fun x => f x (η x)) X :=
    lowerSemicontinuousOn_of_forall_isMaxOn_and_mem hfy η_mem η_max
  obtain ⟨a, ha, ha'⟩ : ∃ a ∈ X, IsMinOn (fun x ↦ f x (η x)) X a := hlsc.exists_isMinOn ne_X kX
  use a, ha
  have hmin_x (y) (hy : y ∈ Y) : ∃ x ∈ X, IsMinOn (f · y) X x := (hfy y hy).exists_isMinOn ne_X kX
  choose! ξ ξ_mem ξ_min using hmin_x
  have husc := upperSemicontinuousOn_of_forall_isMinOn_and_mem hfx ξ_mem ξ_min
  obtain ⟨b, hb, hb'⟩ : ∃ b ∈ Y, IsMaxOn (fun y ↦ f (ξ y) y) Y b := husc.exists_isMaxOn ne_Y kY
  use b, hb
  intro x hx y hy
  calc f a y ≤ f a (η a) := isMaxOn_iff.mp (η_max a ha) y hy
    _ = f (ξ b) b :=
      minimax ne_X kX hfy hfy' cY hfx hfx' cX
        _ (fun x hx ↦ (η_max x hx).isLUB (η_mem x hx))
        _ (ha'.isGLB ha)
        _ (fun y hy ↦ (ξ_min y hy).isGLB (ξ_mem y hy))
        _ (hb'.isLUB hb)
    _ ≤ f x b := isMinOn_iff.mp (ξ_min b hb) x hx

Goal state after: