-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 ⋯))
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 ⋯) :
            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 ⋯))) →
    ∀ (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 ⋯) :
              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 ⋯)))
      (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 ⋯) :
              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 ⋯))),
      Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
        (if h : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ 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 ⋯))

Tactic:
refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩