awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirectedInverseSystem
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)
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)
⊢ 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Order.DirectedInverseSystem
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
k : ι
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)

Tactic:
simp [InverseSystem.map_self]

Premises used: InverseSystem.map_self
-- Module: Mathlib.Order.DirectedInverseSystem
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
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 : ι))
⊢ 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)

Tactic:
funext l
-- Module: Mathlib.Order.DirectedInverseSystem
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)
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 : ι))
⊢ 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:
simp_rw [piEquivLim, piSplitLE_lt hk, piSplitLE_eq, Equiv.trans_apply]

Premises used: Equiv.trans_apply, InverseSystem.piSplitLE_eq, InverseSystem.piSplitLE_lt, InverseSystem.piEquivLim
-- Module: Mathlib.Order.DirectedInverseSystem
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)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) (↑l : ι) ⋯) : ι) <
    (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) k hk) : ι)

Tactic:
l.2

Premises used: Set.Mem, setOf, Set.Iio, Subtype.property
-- Module: Mathlib.Order.DirectedInverseSystem
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)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) (↑l : ι) ⋯) : ι) <
    (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio j) k hk) : ι)

Tactic:
exact l.2

Premises used: Subtype.property
-- Module: Mathlib.Order.DirectedInverseSystem
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
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 ⋯) :
          (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)
⊢ 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)

Tactic:
rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]

Premises used: InverseSystem.piSplitLE_lt, InverseSystem.piEquivLim, LE.le.trans_lt
-- Module: Mathlib.Order.DirectedInverseSystem
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) : ι))
    (((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 ⋯) :
          (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:
apply nat
-- Module: Mathlib.Order.DirectedInverseSystem
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 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_2 : WellFoundedLT ι
h : IsLowerSet (s ∩ t)
e₁ : PEquivOn (F := F) (X := X) f equivSucc s
e₂ : PEquivOn (F := F) (X := X) f equivSucc t
i : ι
his : i ∈ s
hit : i ∈ t
⊢ Eq (α :=
    F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i his) : ι) ≃
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i his) : ι))
    (e₁.equiv (F := F) (X := X) (s := s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i his))
    (e₂.equiv (F := F) (X := X) (s := t) (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hit))

Tactic:
show (e₁.restrict inter_subset_left).equiv ⟨i, his, hit⟩ =
       (e₂.restrict inter_subset_right).equiv ⟨i, his, hit⟩ from
  congr_fun (congr_arg _ <| unique_pEquivOn h) _

Premises used: InverseSystem.PEquivOn.equiv, Subtype.mk, congr_arg, And.intro, congr_fun, InverseSystem.unique_pEquivOn
-- Module: Mathlib.Order.DirectedInverseSystem
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)
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 ⋯) :
          ι))
      ((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)

Tactic:
obtain eq | lt := hsj.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Order.DirectedInverseSystem
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⁺
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 ⋯) : ι))
      ((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 ⋯) :
        X
          (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) i ⋯) :
            ι))
      (((equivSucc hj : (a : F i⁺) → F i × X i) x).2 : X 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)

Tactic:
cases (succ_eq_succ_iff_of_not_isMax hj hi).mp eq

Premises used: Iff.mp, Order.succ_eq_succ_iff_of_not_isMax
-- Module: Mathlib.Order.DirectedInverseSystem
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
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 ⋯) : ι))
    ((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 ⋯) :
      X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hsj) : ι)) i ⋯) : ι))
    (((equivSucc hj : (a : F i⁺) → F i × X i) x).2 : X i)

Tactic:
simp [piEquivSucc]

Premises used: InverseSystem.piEquivSucc
-- Module: Mathlib.Order.DirectedInverseSystem
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 : ι_1
h_1 : i_1 ≤ j_1
ι : 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 : ι))
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι) <
    (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑(hi.mid ⋯) : ι) ⋯) : ι)

Tactic:
h.trans_lt (hi.mid _).2.1

Premises used: Order.IsSuccPrelimit.mid, And.left, LE.le.trans_lt, Subtype.property
-- Module: Mathlib.Order.DirectedInverseSystem
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 : ι))
i_2 : ι
hj : i_2⁺ ∈ Iio i
k : (↑(Ioo i_2⁺ i) : Type u_6)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι) <
    (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι)

Tactic:
k.2.1

Premises used: Order.succ, And.left, Subtype.property
-- Module: Mathlib.Order.DirectedInverseSystem
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 : ι))
i_2 : ι
hj : i_2⁺ ∈ Iio i
k : (↑(Ioo i_2⁺ i) : Type u_6)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι) <
    (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι)

Tactic:
exact k.2.1

Premises used: And.left, Subtype.property