awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
equivLim : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7))
hi : IsSuccPrelimit i
inst_1 : InverseSystem (F := F) f
H :
  ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
    (↑((equivLim : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
j k : ι
hj : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
inl :
  ∀ {equiv : (j_1 : (↑(Iio j) : Type u_6)) → F (↑j_1 : ι) ≃ piLT X (↑j_1 : ι)}
    (nat : IsNatEquiv (F := F) (X := X) f (s := Iio j) equiv)
    {equivLim : F j ≃ (↑(limit (F := F) f j) : Type (max u_6 u_7))} (hi : IsSuccPrelimit j)
    (H :
      ∀ (x : F j) (l : (↑(Iio j) : Type u_6)),
        (↑((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) x) : (l : (↑(Iio j) : Type u_6)) → F (↑l : ι))
            l =
          f ⋯ x)
    (hj : j ∈ Iic j) (hk : k ∈ Iic j),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
      ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) :
            (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
          (f h t) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
      (piLTProj (X := X) h
          ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
              (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
            t) :
        piLT X k)
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
have inr : ∀ (hj_1 : j < i),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
Tactic: obtain rfl | hj := hj.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : InverseSystem (F := F) f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : (↑(Iio j) : Type u_6)) → F (↑j_1 : ι) ≃ piLT X (↑j_1 : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio j) equiv
equivLim : F j ≃ (↑(limit (F := F) f j) : Type (max u_6 u_7))
hi : IsSuccPrelimit j
H :
  ∀ (x : F j) (l : (↑(Iio j) : Type u_6)),
    (↑((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) x) : (l : (↑(Iio j) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
hj : j ∈ Iic j
hk : k ∈ Iic j
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
have inl : ∀ (h : k ≤ k) (t : F k) {equiv : (j : (↑(Iio k) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)}
  (nat : IsNatEquiv (F := F) (X := X) f (s := Iio k) equiv)
  {equivLim : F k ≃ (↑(limit (F := F) f k) : Type (max u_6 u_7))} (hi : IsSuccPrelimit k)
  (H :
    ∀ (x : F k) (l : (↑(Iio k) : Type u_6)),
      (↑((equivLim : (a : F k) → (↑(limit f k) : Type (max u_6 u_7))) x) : (l : (↑(Iio k) : Type u_6)) → F (↑l : ι)) l =
        f sorry x)
  (hj hk : k ∈ Iic k),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hj) :
            (a : F (↑⟨k, hj⟩ : ι)) → piLT X (↑⟨k, hj⟩ : ι))
          t) :
      piLT X k)
Tactic: obtain rfl | hk := hk.eq_or_lt
Cleared hypotheses: j, h, t, equiv, nat, equivLim, hi, H, hj, hk
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : InverseSystem (F := F) f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : (↑(Iio j) : Type u_6)) → F (↑j_1 : ι) ≃ piLT X (↑j_1 : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio j) equiv
equivLim : F j ≃ (↑(limit (F := F) f j) : Type (max u_6 u_7))
hi : IsSuccPrelimit j
H :
  ∀ (x : F j) (l : (↑(Iio j) : Type u_6)),
    (↑((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) x) : (l : (↑(Iio j) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
hj : j ∈ Iic j
hk : k ∈ Iic j
inl :
  ∀ (h : k ≤ k) (t : F k) {equiv : (j : (↑(Iio k) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)}
    (nat : IsNatEquiv (F := F) (X := X) f (s := Iio k) equiv)
    {equivLim : F k ≃ (↑(limit (F := F) f k) : Type (max u_6 u_7))} (hi : IsSuccPrelimit k)
    (H :
      ∀ (x : F k) (l : (↑(Iio k) : Type u_6)),
        (↑((equivLim : (a : F k) → (↑(limit f k) : Type (max u_6 u_7))) x) : (l : (↑(Iio k) : Type u_6)) → F (↑l : ι))
            l =
          f ⋯ x)
    (hj hk : k ∈ Iic k),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) : ι))
      ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) :
            (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
          (f h t) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hk) : ι))
      (piLTProj (X := X) h
          ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic k) k hj) :
              (a : F (↑⟨k, hj⟩ : ι)) → piLT X (↑⟨k, hj⟩ : ι))
            t) :
        piLT X k)
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
have inl₁ : ∀ (hk_1 : k < j),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
Tactic: obtain rfl | hk := hk.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : InverseSystem (F := F) f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : (↑(Iio j) : Type u_6)) → F (↑j_1 : ι) ≃ piLT X (↑j_1 : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio j) equiv
equivLim : F j ≃ (↑(limit (F := F) f j) : Type (max u_6 u_7))
hi : IsSuccPrelimit j
H :
  ∀ (x : F j) (l : (↑(Iio j) : Type u_6)),
    (↑((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) x) : (l : (↑(Iio j) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
hj : j ∈ Iic j
hk_1 : k ∈ Iic j
hk : k < j
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t) :
      piLT X k)
have inl : ∀ (l : (↑(Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) : ι)) : Type u_6)),
  Eq.{u_8 + 1} (α := X (↑l : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h t) l :
      X (↑l : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t)
        l :
      X (↑l : ι))
Tactic: funext l
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : InverseSystem (F := F) f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : (↑(Iio j) : Type u_6)) → F (↑j_1 : ι) ≃ piLT X (↑j_1 : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio j) equiv
equivLim : F j ≃ (↑(limit (F := F) f j) : Type (max u_6 u_7))
hi : IsSuccPrelimit j
H :
  ∀ (x : F j) (l : (↑(Iio j) : Type u_6)),
    (↑((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) x) : (l : (↑(Iio j) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
hj : j ∈ Iic j
hk_1 : k ∈ Iic j
hk : k < j
l : (↑(Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) : ι)) : Type u_6)
⊢ Eq.{u_8 + 1} (α := X (↑l : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h t) l :
      X (↑l : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          t)
        l :
      X (↑l : ι))
have inl : Eq.{u_8 + 1} (α := X (↑l : ι))
  (((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) k hk) :
          F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) k hk) : ι) ≃
            piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) k hk) : ι)) :
        (a : F k) → piLT X k)
      (f h t) l :
    X (↑l : ι))
  (piLTProj (X := X) h
      ((Equiv.symm (piLTLim (X := X) hi) : (a : (↑(limit piLTProj j) : Type (max u_6 u_8))) → piLT X j)
        ((invLimEquiv (F := F) (X := X) nat :
            (a : (↑(limit f j) : Type (max u_6 u_7))) → (↑(limit piLTProj j) : Type (max u_6 u_8)))
          ((equivLim : (a : F j) → (↑(limit f j) : Type (max u_6 u_7))) t)))
      l :
    X (↑l : ι))
Tactic: simp_rw [piEquivLim, piSplitLE_lt hk, piSplitLE_eq, Equiv.trans_apply]
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
equivLim : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7))
hi : IsSuccPrelimit i
inst_1 : InverseSystem (F := F) f
H :
  ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
    (↑((equivLim : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
j k : ι
hj_1 : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h t) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivLim (F := F) (X := X) nat equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) j hj_1) :
            (a : F (↑⟨j, hj_1⟩ : ι)) → piLT X (↑⟨j, hj_1⟩ : ι))
          t) :
      piLT X k)
have inr : Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
  (((equiv, equivLim.trans ((invLimEquiv (F := F) (X := X) nat).trans (Equiv.symm (piLTLim (X := X) hi)))).1
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k sorry) :
        (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
      (f h t) :
    piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) k hk) : ι))
  (piLTProj (X := X) h
      (((equiv, equivLim.trans ((invLimEquiv (F := F) (X := X) nat).trans (Equiv.symm (piLTLim (X := X) hi)))).1
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) j hj) :
          (a : F (↑⟨j, hj_1⟩ : ι)) → piLT X (↑⟨j, hj_1⟩ : ι))
        t) :
    piLT X k)
Tactic: rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
inst_4 : InverseSystem (F := F) f
hi : ¬IsMax i
e : PEquivOn (F := F) (X := X) f equivSucc (Iic i)
H : ∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F i⁺), ((equivSucc hi : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i⁺
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have inl : ∀ (eq : i_2⁺ = i⁺),
  Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
Tactic: obtain eq | lt := hsj.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
inst_4 : InverseSystem (F := F) f
hi : ¬IsMax i
e : PEquivOn (F := F) (X := X) f equivSucc (Iic i)
H : ∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F i⁺), ((equivSucc hi : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i⁺
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)
inl :
  ∀ (eq : i_2⁺ = i⁺),
    Eq.{u_8 + 1} (α :=
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
      ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
            (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
          x
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        X
          (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2
                ⋯) :
            ι))
      (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have inr : ∀ (lt : i_2⁺ < i⁺),
  Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
Tactic: obtain eq | lt := hsj.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
inst_4 : InverseSystem (F := F) f
hi : ¬IsMax i
e : PEquivOn (F := F) (X := X) f equivSucc (Iic i)
H : ∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F i⁺), ((equivSucc hi : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i⁺
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)
eq : i_2⁺ = i⁺
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have inl : ∀ (hsj : i⁺ ∈ Iic i⁺) (hj : ¬IsMax i) (x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) (eq : i⁺ = i⁺),
  Eq.{u_8 + 1} (α :=
    X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) i sorry) : ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) :
          (a : F (↑⟨i⁺, hsj⟩ : ι)) → piLT X (↑⟨i⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) i sorry) :
      X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) i sorry) : ι))
    (((equivSucc hj : (a : F i⁺) → F i × X i) x).2 : X i)
Tactic: cases (succ_eq_succ_iff_of_not_isMax hj hi).mp eq
Cleared hypotheses: i_2, hsj, hj, x, eq
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : (↑(Iio i) : Type u_6)) → PEquivOn (F := F) (X := X) f equivSucc (Iic (↑j : ι))
inst_4 : InverseSystem (F := F) f
equivLim : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7))
H :
  ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
    (↑((equivLim : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
      f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivLim (F := F) (X := X) ⋯ equivLim hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have rw : Eq.{u_8 + 1} (α :=
  X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 sorry) : ι))
  ((((pEquivOnGlue (F := F) (X := X) hi e).equiv (F := F) (X := X) (s := Iio i),
              equivLim.trans ((invLimEquiv (F := F) (X := X) sorry).trans (Equiv.symm (piLTLim (X := X) hi)))).1
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ sorry) :
        (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
      x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 sorry) :
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i_2⁺ hsj) : ι)) i_2 sorry) :
        ι))
  (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
Tactic: rw [piEquivLim, piSplitLE_lt (hi.succ_lt <| (succ_le_iff_of_not_isMax hj).mp hsj)]