mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one
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)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.zero (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f

Tactic:
cases f

Goal state after:
case zero.one.left
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)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.zero (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left

case zero.one.right
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)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.zero (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.zero
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)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn WalkingParallelPair.zero (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f

Tactic:
cases f

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

Goal state before:
pp: case one.one
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)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f

Tactic:
cases f

Goal state after:
case one.one.id
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)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x✝ x : X ⊕ Y
⊢ IsClosed {f | f (x✝, x) ≤ ↑(maxVar X Y)}

Tactic:
apply I3 _ _

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x✝ x : X ⊕ Y
⊢ IsClosed {f | f (x✝, x) ≤ ↑(maxVar X Y)}
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
n : ℕ
⊢ GlueSpace ⋯ ⋯ = (Y (n + 1)).Space

Tactic:
dsimp only [Y, auxGluing]

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 ⋯
n : ℕ
x y : GlueSpace ⋯ ⋯
⊢ edist (c n x) (c n y) = edist x y

Tactic:
dsimp only [Y, auxGluing]

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 ⋯
n : ℕ
x y : GlueSpace ⋯ ⋯
⊢ edist (c n x) (c n y) = edist x y
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst✝²] V₁
V₂_cl : IsClosed[inst✝²] V₂
U₁_op : IsOpen[inst✝²] U₁
U₂_op : IsOpen[inst✝²] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst✝²] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ ∀ x ∈ diagonal γ, W ∈ 𝓝 x

Tactic:
rintro ⟨z, z'⟩ hzz'

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst✝²] V₁
V₂_cl : IsClosed[inst✝²] V₂
U₁_op : IsOpen[inst✝²] U₁
U₂_op : IsOpen[inst✝²] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst✝²] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z z' : γ
hzz' : (z, z') ∈ diagonal γ
⊢ W ∈ 𝓝 (z, z')
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
ne_Y : Y.Nonempty
t : β
x : E
hx : x ∈ X
hx' : ∀ i ∈ Y, f x i ≤ t
c : β
hc : c ∈ lowerBounds {x | ∃ x_1 ∈ X, sup_y x_1 = x}
htc : t < c
⊢ False

Tactic:
simp only [mem_lowerBounds, mem_ofPred_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hc

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✝¹⁰ : 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
ne_Y : Y.Nonempty
t : β
x : E
hx : x ∈ X
hx' : ∀ i ∈ Y, f x i ≤ t
c : β
htc : t < c
hc : ∀ a ∈ X, c ≤ sup_y a
⊢ False