mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : X
this✝ : f (inl x) ∈ ↑p
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
y : Y
hy : Ψ y = z
⊢ BddBelow (range fun y ↦ Fb (inl x, inr y))

Tactic:
simpa only [add_zero] using HD_below_aux1 0

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)
⊢ x = y

Tactic:
have eΨ := cast T Ψisom.isometryEquivOnRange.symm

Goal state after:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)
eΨ : ↑(range Φ) ≃ᵢ y.Rep
⊢ x = y
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)
h : C(X, ℝ) := { toFun := fun x ↦ ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n), continuous_toFun := ⋯ }
x : X
⊢ h x = ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n)

Tactic:
by simp [h]

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
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
⊢ toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f

Tactic:
apply NatTrans.ext

Goal state after:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
⊢ (toSkyscraperPresheaf p₀ (fromStalk p₀ f)).app = f.app
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mp
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 : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T → ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))

Tactic:
intro hT

Goal state after:
case mp
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 : IsLocallySurjective T
⊢ ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
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 : ℱ ⟶ 𝒢
⊢ (∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))) → IsLocallySurjective T

Tactic:
intro hT

Goal state after:
case mpr
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))
⊢ IsLocallySurjective T
Module: Mathlib.Topology.Sheaves.Points

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ∀ {X_1 : Opens X},
    ∀ R ∈ (grothendieckTopology X) X_1,
      ∀
        (x_1 :
          { obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)), map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } },
                map_id := ⋯, map_comp := ⋯ }.obj
            X_1),
        ∃ Y f,
          ∃ (_ : R.arrows f),
            ∃ y,
              (ConcreteCategory.hom
                    ({ obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)),
                          map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }.map
                      f))
                  y =
                x_1

Tactic:
rintro U R hR ⟨⟨hU⟩⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
U : Opens X
R : Sieve U
hR : R ∈ (grothendieckTopology X) U
hU : x ∈ U
⊢ ∃ Y f,
    ∃ (_ : R.arrows f),
      ∃ y,
        (ConcreteCategory.hom
              ({ obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)), map := fun {X_1 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } },
                    map_id := ⋯, map_comp := ⋯ }.map
                f))
            y =
          { down := { down := hU } }
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
⊢ ⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g

Tactic:
by
  obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow
  have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x)
  obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow
  have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)
  -- prove the inequality but with `dist f g` inside, by using inequalities comparing
  -- iSup to iSup and iInf to iInf
  have Z : (⨆ x, ⨅ y, f (inl x, inr y)) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g :=
    ciSup_mono (HD_bound_aux1 _ (dist f g)) fun x =>
      ciInf_mono ⟨cf, forall_mem_range.2 fun i => Hcf _⟩ fun y => coe_le_coe_add_dist
  -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
  -- (here the addition of `dist f g`) preserve infimum and supremum
  have E1 : ∀ x, (⨅ y, g (inl x, inr y)) + dist f g = ⨅ y, g (inl x, inr y) + dist f g := by
    intro x
    refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · change BddBelow (range fun y : Y => g (inl x, inr y))
      exact ⟨cg, forall_mem_range.2 fun i => Hcg _⟩
  have E2 : (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g = ⨆ x, (⨅ y, g (inl x, inr y)) + dist f g := by
    refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · simpa using HD_bound_aux1 _ 0
  -- deduce the result from the above two steps
  simpa [E2, E1, Function.comp]

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₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ ((γ.subpath t₀ (Icc.convexComb t₁ t₂ x.1)).trans (γ.subpath (Icc.convexComb t₁ t₂ x.1) t₂)) x.2

Tactic:
refine Path.trans_continuous_family γ₁ ?_ γ₂ ?_ <;>
    refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)

Goal state after:
case refine_1.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ t₀

case refine_1.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ ⟨(1 - ↑x.1) * ↑t₁ + ↑x.1 * ↑t₂, ⋯⟩

case refine_1.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ x.2

case refine_2.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ ⟨(1 - ↑x.1) * ↑t₁ + ↑x.1 * ↑t₂, ⋯⟩

case refine_2.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ t₂

case refine_2.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ x.2
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
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f x y ≤ sup_y x

Tactic:
exact (hsup_y x hx).1 ⟨y, hy, rfl⟩

Goal state after: