awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
x : F i⁺
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:
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
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
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 : ι))
⊢ 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)

Tactic:
funext l
-- 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
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)
inl :
  Eq.{u_8 + 1} (α := X (↑l : ι))
    (piLTProj (X := X) hk
      ((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯) : (a : F (↑⟨i, ⋯⟩ : ι)) → piLT X (↑⟨i, ⋯⟩ : ι))
        ((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 : ι) ⋯),
              e.trans
                (Equiv.trans
                  (Equiv.prodCongr (equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) (Equiv.refl (X i)))
                  (Equiv.trans (piSplitLE (X := X))
                    (Equiv.piCongrSet (W := X) (s :=
                      Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯ : { x : ι // x ∈ Iic i }) : ι)) (t := Iio i⁺)
                      ⋯))))
            (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 : ι) ⋯))
⊢ 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:
rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]

Premises used: le_rfl, InverseSystem.piEquivSucc, InverseSystem.map_map, InverseSystem.piSplitLE_lt, InverseSystem.piLTProj, Order.le_succ
-- 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
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 : ι))
    (piLTProj (X := X) hk
      ((equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯) : (a : F (↑⟨i, ⋯⟩ : ι)) → piLT X (↑⟨i, ⋯⟩ : ι))
        ((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 : ι) ⋯),
              e.trans
                (Equiv.trans
                  (Equiv.prodCongr (equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) (Equiv.refl (X i)))
                  (Equiv.trans (piSplitLE (X := X))
                    (Equiv.piCongrSet (W := X) (s :=
                      Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯ : { x : ι // x ∈ Iic i }) : ι)) (t := Iio i⁺)
                      ⋯))))
            (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 : ι) ⋯))

Tactic:
simp [piSplitLE_lt (l.2.trans_le hk)]

Premises used: LT.lt.trans_le, InverseSystem.piSplitLE_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_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 : ι)
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 : ι))
⊢ 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))

Tactic:
simp_rw [← t.2 h]

Premises used: 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_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 : ι))
    ((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:
apply nat
-- 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_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)
hj : (↑x_1 : ι) ∈ Iio i
⊢ (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

Tactic:
rw [nat, ← t.2 h]

Premises used: 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_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 : ι)
⊢ 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)

Tactic:
simp
-- 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_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 : ι)
⊢ (↑x_1 : ι) ∈ Iio i

Tactic:
simp
-- 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
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 : (↑(Iio i) : Type u_6)
⊢ (↑((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 }))
            ((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 }))
              t)) :
        (l : (↑(Iio i) : Type u_6)) → F (↑l : ι))
      x =
    (↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) x

Tactic:
apply Equiv.left_inv

Premises used: Equiv.left_inv
-- 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
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))
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))
                ⋯ :
              { 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)) :
      (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
⊢ (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

Tactic:
ext1
-- 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
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 : (↑(Iio i) : Type u_6)
⊢ (↑((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)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      x =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x

Tactic:
apply Equiv.right_inv

Premises used: Equiv.right_inv
-- 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 : 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)
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)
⊢ 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

Premises used: LE.le.eq_or_lt, rfl