mathlib-initiative/mathlib-tactics huggingface dataset:
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)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
⊢ 1 / 2 / 2 ^ i = (f i) x * (1 / 2 / 2 ^ i)

Tactic:
by simp [hfu i hi]

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
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
hpq' : (F p).snd ≍ (F q).snd
⊢ (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩

Tactic:
rw [Fin.heq_fun₂_iff Npq Npq] at hpq'

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
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
hpq' : ∀ (i j : Fin (N p)), (F p).snd i j = (F q).snd ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
⊢ (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩
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
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
⊢ ∀ᶠ (b : F.EtaleSpace) in 𝓝 ↑⟨g, hg⟩,
    ∀ (a : ↑(base ⁻¹' ↑U)),
      ↑a = b →
        WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑a).germ)) =
          WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑⟨g, hg⟩).germ))

Tactic:
rcases hF_bij _ hg |>.surjective g.germ with ⟨f, hf⟩

Goal state after:
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
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
⊢ ∀ᶠ (b : F.EtaleSpace) in 𝓝 ↑⟨g, hg⟩,
    ∀ (a : ↑(base ⁻¹' ↑U)),
      ↑a = b →
        WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑a).germ)) =
          WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑⟨g, hg⟩).germ))
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 : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
set t_x := 𝒢.germ _ x hxU t with ht_x

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))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:

Tactic:
⨅ y, f (inl x, inr y) + C ≤ f (inl x, inr default) + C := ciInf_le (HD_below_aux1 C) default
    _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

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

Goal state before:
pp: case op.op.single.single.id_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 (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (id_single i)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (id_single i))

Tactic:
dsimp
          rw [F.map_id]
          simp

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

Goal state before:
pp: case op.op.pair.pair.id_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 (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (id_pair a✝¹ a✝)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (id_pair a✝¹ a✝))

Tactic:
dsimp
          rw [F.map_id]
          simp

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
⊢ (fun p ↦ dist p.1 p.2) ∈ candidates X Y

Tactic:
simp_rw [candidates, Set.mem_ofPred_eq, dist_comm, dist_triangle, dist_self, maxVar_bound,
    forall_const, and_true]
  exact ⟨fun x y => rfl, fun x y => rfl⟩

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

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
hpq' : (F p).snd ≍ (F q).snd
⊢ ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)

Tactic:
rw [Fin.heq_fun₂_iff Npq Npq] at hpq'

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
hpq' : ∀ (i j : Fin (N p)), (F p).snd i j = (F q).snd ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
⊢ ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : Fin 1 → X
F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = refl (p 0)

Tactic:
rw [concat, dfoldl_zero]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    i.fst.Finite →
      (∀ (a : ι) (b : a ∈ i.fst), i.snd ⟨a, b⟩ ∈ uniformity X) →
        (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsSymm) →
          (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsTrans) →
            SetRel.IsSymm (⋂ i_1, ⋂ (h : i_1 ∈ i.fst), i.snd ⟨i_1, h⟩)

Tactic:
rintro _ _ _ _ _

Goal state after:
case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
i✝ : (I : Set ι) × (↑I → SetRel X X)
a✝³ : i✝.fst.Finite
a✝² : ∀ (a : ι) (b : a ∈ i✝.fst), i✝.snd ⟨a, b⟩ ∈ uniformity X
a✝¹ : ∀ (a : ι) (b : a ∈ i✝.fst), (i✝.snd ⟨a, b⟩).IsSymm
a✝ : ∀ (a : ι) (b : a ∈ i✝.fst), (i✝.snd ⟨a, b⟩).IsTrans
⊢ SetRel.IsSymm (⋂ i, ⋂ (h : i ∈ i✝.fst), i✝.snd ⟨i, h⟩)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    i.fst.Finite →
      (∀ (a : ι) (b : a ∈ i.fst), i.snd ⟨a, b⟩ ∈ uniformity X) →
        (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsSymm) →
          (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsTrans) →
            SetRel.IsTrans (⋂ i_1, ⋂ (h : i_1 ∈ i.fst), i.snd ⟨i_1, h⟩)

Tactic:
rintro _ _ _ _ _

Goal state after:
case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
i✝ : (I : Set ι) × (↑I → SetRel X X)
a✝³ : i✝.fst.Finite
a✝² : ∀ (a : ι) (b : a ∈ i✝.fst), i✝.snd ⟨a, b⟩ ∈ uniformity X
a✝¹ : ∀ (a : ι) (b : a ∈ i✝.fst), (i✝.snd ⟨a, b⟩).IsSymm
a✝ : ∀ (a : ι) (b : a ∈ i✝.fst), (i✝.snd ⟨a, b⟩).IsTrans
⊢ SetRel.IsTrans (⋂ i, ⋂ (h : i ∈ i✝.fst), i✝.snd ⟨i, h⟩)