-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀
    (h :
      ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
        Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
          (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
          else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯)))
    (i : ι) (hi : i ≤ a),
    Membership.mem (γ := Set (X i))
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : ι)))
      (x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i ⋯))
h₁ :
  ∀
    (h :
      ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
        Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
          (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
          else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯)))
    (i : ι),
    a < i ∧ i ≤ b →
      ∀ (hi1 : a < i) (hi2 : i ≤ b),
        Membership.mem (γ := Set (X i))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i ⋯))
⊢ (∀ (a_1 : ι) (b_1 : a_1 ≤ b),
      Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
        (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))) ↔
    (∀ (a_1 : ι) (b_1 : a_1 ≤ a),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 ⋯))) ∧
      ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))
have h₂ : ((∀ (a_1 : ι) (b_1 : a_1 ≤ a),
      Membership.mem (γ := Set (X a_1))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
        (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 sorry))) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
      Membership.mem (γ := Set (X a_1))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
        (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 sorry))) →
  ∀ (i : ι) (hi : i ≤ b)
    (h1 :
      ∀ (a_1 : ι) (b_1 : a_1 ≤ a),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 sorry)))
    (h2 :
      ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
          (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 sorry))),
    Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i sorry))
      (if h : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) i sorry))
Tactic: refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩