mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

Tactic:
rintro ⟨H⟩

Goal state after:
case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
H : (↑a₁).HomotopyRel (↑a₂) (Cube.boundary N)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂) →
    (Homotopic.setoid N x) a₁ a₂

Tactic:
rintro ⟨H⟩

Goal state after:
case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
H : Path ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)
⊢ (Homotopic.setoid N x) a₁ a₂
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

Tactic:
rintro ⟨H⟩

Goal state after:
case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : (↑a₁).HomotopyRel (↑a₂) (Cube.boundary N)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂) →
    (Homotopic.setoid N x) a₁ a₂

Tactic:
rintro ⟨H⟩

Goal state after:
case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ (Homotopic.setoid N x) a₁ 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
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(maxVar X Y) * max (dist x z) (dist t y) + ↑(maxVar X Y) * max (dist x z) (dist t y) =
    2 * ↑(maxVar X Y) * max (dist x z) (dist y t)

Tactic:
rw [dist_comm t y]
      ring

Goal state after:
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:
by
  simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s).offDiag.toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)

Tactic:
← Finset.coe_offDiag,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s.offDiag).toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case right
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ (range fun x ↦ ↑(f x)) = ↑p

Tactic:
range_comp',

Goal state after:
case right
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ Subtype.val '' range ⇑f = ↑p
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
rw [Set.infsep_of_fintype, dif_pos hs]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s).offDiag.Nonempty ↔ s.offDiag.Nonempty

Tactic:
← Finset.coe_offDiag,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s.offDiag).Nonempty ↔ s.offDiag.Nonempty
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.inf' hs (uncurry dist)

Tactic:
← Finset.coe_offDiag,

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ ((↑s.offDiag).toFinset.inf' ⋯ fun x ↦ uncurry dist x) = s.offDiag.inf' hs (uncurry dist)
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
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧

Tactic:
have I :
      (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) =
        (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl

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
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
I :
  (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ IsBounded (⇑toSnowflaking ⁻¹' s) ↔ IsBounded s

Tactic:
rw [← image_ofSnowflaking_eq_preimage, isBounded_image_ofSnowflaking_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
⊢ ∀ s ∈ {s | ∃ a, (Ici a)ᶜ = s}, IsOpen[inst✝¹] (⇑toLower ⁻¹' s)

Tactic:
by rintro _ ⟨a, rfl⟩; exact isClosed_Ici.isOpen_compl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s

Tactic:
topology_eq α

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[upperSet α] s ↔ IsUpperSet s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s

Tactic:
topology_eq α

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen[lower α] s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}

Tactic:
rw [sUnion_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ Continuous[inst✝³, inst✝²] f

Tactic:
simp_rw [continuous_def, isOpen_iff_isUpperSet]
  intro s hs
  exact (IsUpper.isUpperSet_of_isOpen hs).preimage hf

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ IsLowerSet s

Tactic:
topology_eq α

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[lowerSet α] s ↔ IsLowerSet s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s

Tactic:
topology_eq α

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
s : Set α
⊢ IsOpen[upper α] s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ Uᶜ ⊆ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ⊆ Uᶜ

Tactic:
refine ⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset ?_⟩

Goal state after:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ sSup Uᶜ ∈ Uᶜ
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iic

Tactic:
have : Nonempty (Ioi a) :=
    (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
  refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis
    (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)
  simpa only [Iic_subset_Iio] using! Filter.nonempty_of_mem (Ioo_mem_nhdsGT hc)

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

Goal state before:
pp: case neg
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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
h : ¬hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
calc
        hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            HD (candidatesBDist X Y) :=
          hausdorffDist_optimal_le_HD _ _ candidatesBDist_mem_candidatesB
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := HD_candidatesBDist_le
        _ ≤ hausdorffDist (p : Set ℓ_infty_ℝ) q := not_lt.1 h

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

Goal state before:
pp: δ : ℝ
δ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
⊢ dist p q ≤ δ

Tactic:
have Npq : N p = N q := (Sigma.mk.inj_iff.1 hpq).1

Goal state after:
δ : ℝ
δ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
⊢ dist p q ≤ δ
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 y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
⊢ ((Functor.const (StructuredArrow (Opposite.op (iSup Us)) (principals X))).obj S.pt).map e ≫
      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) ≫
        limit.π (generator (principalOpen x.right) ⋙ F)
          { left := { as := PUnit.unit }, right := x.right,
            hom := 𝟙 ((fromPUnit (Opposite.op (principalOpen x.right))).obj { as := PUnit.unit }) }) ≫
      (generator (iSup Us) ⋙ F).map e

Tactic:
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]

Goal state after:
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 y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
⊢ S.π.app ((projSup Us).obj y) ≫
      limit.π (generator (principalOpen y.right) ⋙ F)
        { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) } =
    S.π.app ((projSup Us).obj x) ≫
      limit.π (generator (principalOpen x.right) ⋙ F)
          { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } ≫
        F.map ((generator (iSup Us)).map e)
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
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
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r

Tactic:
refine hausdorffDist_le_of_mem_dist ?_ A ?_

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
⊢ 0 ≤ r

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
have wUx := wU ⟨x, mU⟩

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
wUx : (fun x_1 ↦ fU (iU x_1)) ⟨x, mU⟩ = (ConcreteCategory.hom (F.germ U' ↑⟨x, mU⟩ ⋯)) gU
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝¹ : S.X₁.IsFlasque
inst✝ : S.X₂.IsFlasque
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₂.obj.map i ≫ S.g.hom.app V)

Tactic:
exact CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)

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

Goal state before:
pp: X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝¹ : S.X₁.IsFlasque
inst✝ : S.X₂.IsFlasque
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₃.obj.map i)

Tactic:
have : Epi (S.g.1.app U ≫ S.X₃.obj.map i) := by
      rw [← S.g.hom.naturality i]
      exact CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)
    exact CategoryTheory.epi_of_epi (S.g.1.app U) (S.X₃.obj.map i)

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
hmn : m ≤ n
H : HasSmallInductiveDimensionLT X m
⊢ HasSmallInductiveDimensionLT X n

Tactic:
by
  induction n generalizing m X with
  | zero => simp_all
  | succ m IH =>
    cases H with
    | zero => exact .succ _ ∅ (by simpa) (by simp)
    | succ n s hs h =>
      refine .succ _ s hs fun U hU ↦ IH ?_ (h U hU)
      rwa [add_le_add_iff_right] at hmn

Goal state after: