awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (hypothesis)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
j k : ι
hj : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          x) :
      piLT X k)
have lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
Tactic: have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
-- 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
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
j k : ι
hj : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          x) :
      piLT X k)
have inl : ∀ (hj : i⁺ ∈ Iic i⁺) (h : k ≤ i⁺) (x : F i⁺),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X k)
Tactic: obtain rfl | hj := le_succ_iff_eq_or_le.mp hj
Cleared hypotheses: j, hj, h, x
-- 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
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
j k : ι
hj : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
inl :
  ∀ (hj : i⁺ ∈ Iic i⁺) (h : k ≤ i⁺) (x : F i⁺),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
      ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
            (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
          (f h x) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
      (piLTProj (X := X) h
          ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
              (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
            x) :
        piLT X k)
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          x) :
      piLT X k)
have inr : ∀ (hj_1 : j ≤ i),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj) :
            (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
          x) :
      piLT X k)
Tactic: obtain rfl | hj := le_succ_iff_eq_or_le.mp hj
-- 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
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
k : ι
hk : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X k)
have inl : ∀ (hk : i⁺ ∈ Iic i⁺) (h : i⁺ ≤ i⁺),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) :
          (a : F (↑⟨i⁺, hk⟩ : ι)) → piLT X (↑⟨i⁺, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X i⁺)
Tactic: obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
Cleared hypotheses: k, hk, h
-- 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
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
k : ι
hk : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
inl :
  ∀ (hk : i⁺ ∈ Iic i⁺) (h : i⁺ ≤ i⁺),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) : ι))
      ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) :
            (a : F (↑⟨i⁺, hk⟩ : ι)) → piLT X (↑⟨i⁺, hk⟩ : ι))
          (f h x) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hk) : ι))
      (piLTProj (X := X) h
          ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
              (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
            x) :
        piLT X i⁺)
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X k)
have inl₁ : ∀ (hk_1 : k ≤ i),
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X k)
Tactic: obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
-- 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
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
k : ι
hk_1 : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x) :
      piLT X k)
have inl : ∀ (l : (↑(Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) : ι)) : Type u_6)),
  Eq.{u_8 + 1} (α := X (↑l : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h x) l :
      X (↑l : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x)
        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
i : ι
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
k : ι
hk_1 : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : (↑(Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) : ι)) : Type u_6)
⊢ Eq.{u_8 + 1} (α := X (↑l : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk_1) :
          (a : F (↑⟨k, hk_1⟩ : ι)) → piLT X (↑⟨k, hk_1⟩ : ι))
        (f h x) l :
      X (↑l : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
            (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
          x)
        l :
      X (↑l : ι))
have inl : Eq.{u_8 + 1} (α := X (↑l : ι))
  (piLTProj (X := X) hk
    ((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry) : (a : F (↑⟨i, sorry⟩ : ι)) → piLT X (↑⟨i, sorry⟩ : ι))
      ((e : (a : F i⁺) → F i × X i) x).1)
    l)
  ((((piSplitLE (X := fun (i : ι) ↦ F i ≃ piLT X i) :
            (a : piLT (fun (i : ι) ↦ F i ≃ piLT X i) i⁺ × (F i⁺ ≃ piLT X i⁺)) →
              (j : (↑(Iic i⁺) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι))
          (fun (j : (↑(Iio i⁺) : Type u_6)) ↦ equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) sorry),
            e.trans
              (Equiv.trans (Equiv.prodCongr (equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry)) (Equiv.refl (X i)))
                (Equiv.trans (piSplitLE (X := X))
                  (Equiv.piCongrSet (W := X) (s :=
                    Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry : { x : ι // x ∈ Iic i }) : ι)) (t := Iio i⁺)
                    sorry))))
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) :
        F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) : ι) ≃
          piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ hj) : ι)) :
      (a : F (↑⟨i⁺, hj⟩ : ι)) → piLT X (↑⟨i⁺, hj⟩ : ι))
    x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) (↑l : ι) sorry))
Tactic: rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]
-- 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_1 : 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
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
t : (↑(limit (F := F) f i) : Type (max u_6 u_7))
x x_1 : (↑(Iio i) : Type u_6)
h : (↑x : ι) ≤ (↑x_1 : ι)
⊢ Eq (α := piLT X (↑x : ι))
    ((fun (l : (↑(Iio i) : Type u_6)) ↦
        ((equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l) :
          piLT X (↑l : ι)))
      x)
    (piLTProj (X := X) h
      ((fun (l : (↑(Iio i) : Type u_6)) ↦
          ((equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l) :
            piLT X (↑l : ι)))
        x_1))
have simp_rw : Eq (α := piLT X (↑x : ι))
  ((equiv x : (a : F (↑x : ι)) → piLT X (↑x : ι)) (f h ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) x_1)) :
    piLT X (↑x : ι))
  (piLTProj (X := X) h
      ((equiv x_1 : (a : F (↑x_1 : ι)) → piLT X (↑x_1 : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) x_1)) :
    piLT X (↑x : ι))
Tactic: simp_rw [← t.2 h]
-- 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_1 : 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
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))
x x_1 : (↑(Iio i) : Type u_6)
h : (↑x : ι) ≤ (↑x_1 : ι)
⊢ (equiv x : (a : F (↑x : ι)) → piLT X (↑x : ι))
      (f h
        ((fun (l : (↑(Iio i) : Type u_6)) ↦
            (((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l) :
              F (↑l : ι)))
          x_1)) =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x
have rw : piLTProj (X := X) h
    ((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑x_1 : ι) sorry) :
        (a : F (↑⟨(↑x_1 : ι), sorry⟩ : ι)) → piLT X (↑⟨(↑x_1 : ι), sorry⟩ : ι))
      ((fun (l : (↑(Iio i) : Type u_6)) ↦
          (((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
              ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l) :
            F (↑l : ι)))
        x_1)) =
  piLTProj (X := X) h ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x_1)
Tactic: rw [nat, ← t.2 h]
-- 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_1 : 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
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))
x x_1 : (↑(Iio i) : Type u_6)
h : (↑x : ι) ≤ (↑x_1 : ι)
rw :
  piLTProj (X := X) h
      ((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑x_1 : ι) ⋯) :
          (a : F (↑⟨(↑x_1 : ι), ⋯⟩ : ι)) → piLT X (↑⟨(↑x_1 : ι), ⋯⟩ : ι))
        ((fun (l : (↑(Iio i) : Type u_6)) ↦
            (((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l) :
              F (↑l : ι)))
          x_1)) =
    piLTProj (X := X) h ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x_1)
⊢ (equiv x : (a : F (↑x : ι)) → piLT X (↑x : ι))
      (f h
        ((fun (l : (↑(Iio i) : Type u_6)) ↦
            (((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l) :
              F (↑l : ι)))
          x_1)) =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x
have hj : (↑x_1 : ι) ∈ Iio i
Tactic: rw [nat, ← t.2 h]
-- 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
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))
⊢ (fun (t : (↑(limit (F := F) f i) : Type (max u_6 u_7))) ↦
        (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) ↦
            Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
              (limit (F := piLT X) (piLTProj (X := X)) i) x)
            (fun (l : (↑(Iio i) : Type u_6)) ↦
              (equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l))
            ⋯ :
          { x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι) //
            Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
              (limit (F := piLT X) (piLTProj (X := X)) i) x }))
      ((fun (t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))) ↦
          (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) ↦ x ∈ limit (F := F) f i)
              (fun (l : (↑(Iio i) : Type u_6)) ↦
                ((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                  ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l))
              ⋯ :
            { x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι) // x ∈ limit (F := F) f i }))
        t) =
    t
have a : (↑((fun (t : (↑(limit (F := F) f i) : Type (max u_6 u_7))) ↦
          (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) ↦
              Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                (limit (F := piLT X) (piLTProj (X := X)) i) x)
              (fun (l : (↑(Iio i) : Type u_6)) ↦
                (equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l))
              sorry :
            { x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι) //
              Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                (limit (F := piLT X) (piLTProj (X := X)) i) x }))
        ((fun (t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))) ↦
            (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) ↦ x ∈ limit (F := F) f i)
                (fun (l : (↑(Iio i) : Type u_6)) ↦
                  ((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                    ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l))
                sorry :
              { x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι) // x ∈ limit (F := F) f i }))
          t)) :
    (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) =
  (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
Tactic: ext1
-- 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
⊢ 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 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 sorry 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)
Tactic: obtain rfl | hj := hj.eq_or_lt
Cleared hypotheses: i, equiv, nat, equivLim, hi, H, hj, hk