mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

Tactic:
simp only [le_refl, true_or, or_true]

Goal state after:
case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

Tactic:
simp only [le_refl, true_or, or_true]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
simp only [le_refl, true_or, or_true]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
simp only [le_refl, true_or, or_true]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: p q : GHSpace
⊢ dist p q = ghDist p.Rep q.Rep

Tactic:
rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]

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∞
⊢ ⇑toSnowflaking '' closedEBall x r = closedEBall (toSnowflaking x) (r ^ α)

Tactic:
rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedEBall]

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
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
inhabit X

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
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ⋂₀ (compl '' S) ⊆ Ici (sSup {a | (Ici a)ᶜ ∈ S})

Tactic:
· intro b hb
      rw [mem_Ici, sSup_le_iff]
      intro c hc
      simp only [sInter_image, mem_iInter] at hb
      rw [← not_lt, ← mem_Iio, ← compl_Ici]
      exact hb _ hc

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩

Tactic:
· by_cases hx : IsPredPrelimit x
      · obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h
        use some z
        simp [some, Prod.Lex.lt_iff, hz', hz]
      obtain ⟨s, hs⟩ := exists_gt (max 0 q)
      rw [max_lt_iff] at hs
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · simp [hx, hs.1.le]
      · simp [Prod.Lex.lt_iff, hs.2, h]

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩
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
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
t₁ t₂ : ↑(𝒫 s)
h : U t₁ ∩ d = U t₂ ∩ d
ht : (↑t₁ \ ↑t₂).Nonempty
hUVd : (U t₂ ∩ d ∩ V t₂).Nonempty
⊢ False

Tactic:
exact hUVd.not_disjoint <| disjoint_of_subset_left inter_subset_left (hUV t₂)

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this : 0 ≤ ε₂
p q : ↑s
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)

Tactic:
by linarith

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this✝ : 0 ≤ ε₂
this : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
⊢ 0 < ε₂ / 2 + δ

Tactic:
by linarith

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
⊢ 0 ≤ ε₂ / 2 + δ

Tactic:
by linarith

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
x : ℝ
h : x ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
⊢ 0 ≤ x

Tactic:
rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩
              exact (hfr x).1

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
A : C
inst✝ : HasTerminal C
⊢ IsTerminal ((skyscraperPresheaf PUnit.unit A).obj (op ⊥))

Tactic:
dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1}

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ RightInverse
    (fun x_1 ↦
      match x_1 with
      | (⟨y, hy⟩, WithTopology.toTopology .(⊥) g) =>
        ⟨{ base := y, germ := (ConcreteCategory.hom (F.germ U y hy)) (surjInv ⋯ g) }, hy⟩)
    fun s ↦ (⟨(↑s).base, ⋯⟩, WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ)))

Tactic:
by
    rintro ⟨⟨y, hy⟩, ⟨g⟩⟩
    simp only
    congr
    rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
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
⊢ (diagram F U).obj WalkingParallelPair.one ≅ (diagram G U).obj WalkingParallelPair.one

Tactic:
exact piInters.isoOfIso U α

Goal state after:
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
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ HD g + dist f g

Tactic:
by grw [HD_lipschitz_aux2 f g, HD, ← le_max_right]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ HD (candidatesBDist X Y) ≤ diam univ + 1 + diam univ

Tactic:
refine max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_)

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
⊢ ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

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
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : CategoryTheory.Pairwise ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫ ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op j) =
    ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op j)

Tactic:
rcases j with ⟨⟩

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op (single a✝)) =
    ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op (single a✝))

case op.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op (Pairwise.pair a✝¹ a✝)) =
    ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op (Pairwise.pair a✝¹ a✝))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ IsCompact (range Quotient.mk')

Tactic:
exact isCompact_range (continuous_sum_dom.2
    ⟨(isometry_optimalGHInjl X Y).continuous, (isometry_optimalGHInjr X Y).continuous⟩)

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : CategoryTheory.Pairwise ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫ ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op j) =
    ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op j)

Tactic:
rcases j with ⟨⟩

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op (single a✝)) =
    ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op (single a✝))

case op.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π.app (op (Pairwise.pair a✝¹ a✝)) =
    ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π.app (op (Pairwise.pair a✝¹ a✝))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
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
⊢ 0 ≤ r

Tactic:
inhabit X

Goal state after:
case refine_1
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
inhabited_h : Inhabited X
⊢ 0 ≤ r
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, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (hz' : z' ∈ segment ℝ ↑y ↑y'), ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ (hz' : z' ∈ segment ℝ ↑y ↑y'),
        x ∈ sublevelLeft X f b' z' ∧ ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
z' : F
hz' : z' ∈ segment ℝ ↑y ↑y'
hxz'1 : x ∈ sublevelLeft X f b' z'
hxz'2 : ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
⊢ ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'

Tactic:
exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩

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

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
let coeZ := ((↑) : Z0 → Z)

Goal state after:
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
⊢ ∃ x, Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
p : Fin (n + 2) → X
F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = (concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))

Tactic:
by
  rw [concat, dfoldl_succ_last]
  rfl

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

Goal state before:
pp: case neg
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 : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
⊢ False

Tactic:
have : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅ := by grind

Goal state after:
case neg
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 : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅
⊢ False