mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
x : X
⊢ BddBelow (range fun y ↦ g (inl x, inr y))

Tactic:
change BddBelow (range fun y : Y => g (inl x, inr y))
      exact ⟨cg, forall_mem_range.2 fun i => Hcg _⟩

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

Goal state before:
pp: 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✝ : ι
⊢ 𝟙 c.pt ≫ (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ Pi.π (fun i ↦ F.obj (op (U i))) a✝ = c.π.app (op (single a✝))

Tactic:
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]

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

Goal state before:
pp: 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✝ : ι
⊢ 𝟙 c.pt ≫
      (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝) =
    c.π.app (op (Pairwise.pair a✝¹ a✝))

Tactic:
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]

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

Goal state before:
pp: 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✝ : ι
⊢ 𝟙 c.pt ≫ c.π.app (op (single a✝)) = (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ Pi.π (fun i ↦ F.obj (op (U i))) a✝

Tactic:
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]

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

Goal state before:
pp: 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✝ : ι
⊢ 𝟙 c.pt ≫ c.π.app (op (Pairwise.pair a✝¹ a✝)) =
    (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝)

Tactic:
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : ¬HasSmallInductiveDimensionLT X n
a : WithBot ℕ∞
ha : a < ↑n
⊢ ∃ i, a < ↑i ∧ ¬HasSmallInductiveDimensionLT X i

Tactic:
exact ⟨n, ha, h⟩

Goal state after: