awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F j → F i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
inst_1 : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
a :
  ∀ (j : (↑(Iio i) : Type u_6)) (l : (↑(Iio (↑j : ι)) : Type u_6)),
    (↑((fun (f : piLT X i) ↦
                (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                  { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                    (l : (↑(Iio i) : Type u_6)) ↦
                  let k := hi.mid ⋯;
                  (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                    (Subtype.mk (p := fun (x : ι) ↦
                      x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι)) (↑l : ι) ⋯))
                f)) :
          (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
        j l =
      (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l
⊢ (fun (f : piLT X i) ↦
        (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
          { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))) (l : (↑(Iio i) : Type u_6)) ↦
          let k := hi.mid ⋯;
          (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
              (↑l : ι) ⋯))
        f) =
    f

Tactic:
ext j l
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F j → F i
i_1 j_1 : ι_1
h : i_1 ≤ j_1
ι : Type u_6
inst_1 : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
j : (↑(Iio i) : Type u_6)
l : (↑(Iio (↑j : ι)) : Type u_6)
k : (↑(Ioo (↑l : ι) i) : Type u_6) := hi.mid ⋯
le : j ≤ Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯
⊢ (↑((fun (f : piLT X i) ↦
              (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                  (l : (↑(Iio i) : Type u_6)) ↦
                let k := hi.mid ⋯;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
                    (↑l : ι) ⋯))
              f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      j l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l

Tactic:
congr_fun (f.2 le) l

Premises used: Set.Mem, congr_fun, 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 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F j → F i
i_1 j_1 : ι_1
h : i_1 ≤ j_1
ι : Type u_6
inst_1 : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
j : (↑(Iio i) : Type u_6)
l : (↑(Iio (↑j : ι)) : Type u_6)
k : (↑(Ioo (↑l : ι) i) : Type u_6) := hi.mid ⋯
le : Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯ ≤ j
⊢ (↑((fun (f : piLT X i) ↦
              (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                  (l : (↑(Iio i) : Type u_6)) ↦
                let k := hi.mid ⋯;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
                    (↑l : ι) ⋯))
              f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      j l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l

Tactic:
(congr_fun (f.2 le) ⟨l, _⟩).symm

Premises used: Set.Mem, Subtype.mk, congr_fun, Eq.symm, Subtype.val, 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 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F j → F i
i_1 j_1 : ι_1
h : i_1 ≤ j_1
ι : Type u_6
inst_1 : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
j : (↑(Iio i) : Type u_6)
l : (↑(Iio (↑j : ι)) : Type u_6)
k : (↑(Ioo (↑l : ι) i) : Type u_6) := hi.mid ⋯
le : j ≤ Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯
⊢ (↑((fun (f : piLT X i) ↦
              (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                  (l : (↑(Iio i) : Type u_6)) ↦
                let k := hi.mid ⋯;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
                    (↑l : ι) ⋯))
              f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      j l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l

Tactic:
exacts [congr_fun (f.2 le) l, (congr_fun (f.2 le) ⟨l, _⟩).symm]

Premises used: Subtype.mk, congr_fun, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
inst : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
k l : (↑(Iio i) : Type u_6)
hl : (↑l : ι) < (↑k : ι)
rw :
  (↑(Equiv.toFun (piLTLim (X := X) hi) (Equiv.invFun (piLTLim (X := X) hi) f)) :
      (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
    k (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)
| (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) k (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)

Tactic:
rw [← (piLTLim hi).right_inv f]

Premises used: Equiv.right_inv, InverseSystem.piLTLim
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
inst : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
k l : (↑(Iio i) : Type u_6)
hl : (↑l : ι) < (↑k : ι)
conv_rhs :
  (Equiv.symm (piLTLim (X := X) hi) : (a : (↑(limit piLTProj i) : Type (max u_6 u_7))) → piLT X i) f l =
    (↑(Equiv.toFun (piLTLim (X := X) hi) (Equiv.invFun (piLTLim (X := X) hi) f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      k (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)
⊢ (Equiv.symm (piLTLim (X := X) hi) : (a : (↑(limit piLTProj i) : Type (max u_6 u_7))) → piLT X i) f l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) k
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)

Tactic:
conv_rhs => rw [← (piLTLim hi).right_inv f]

Premises used: Equiv.right_inv, InverseSystem.piLTLim
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
inst : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
k l : (↑(Iio i) : Type u_6)
hl : (↑l : ι) < (↑k : ι)
⊢ (Equiv.symm (piLTLim (X := X) hi) : (a : (↑(limit piLTProj i) : Type (max u_6 u_7))) → piLT X i) f l =
    (↑(Equiv.toFun (piLTLim (X := X) hi) (Equiv.invFun (piLTLim (X := X) hi) f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      k (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)

Tactic:
rfl
-- 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 : PartialOrder ι
inst_2 : DecidableEq ι
f : piLT X i × X i
fst :
  ∀ (j : (↑(Iio i) : Type u_6)),
    ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
              ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                  f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
                piLT X i × X i))
            ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
                (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
                  else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
                  X (↑j : ι)))
              f)).1
        j =
      f.1 j
snd :
  ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
          ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
              f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
            piLT X i × X i))
        ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
            (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
              else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
              X (↑j : ι)))
          f)).2 =
    f.2
⊢ (fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
        ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
            f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
          piLT X i × X i))
      ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
          (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
            else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
            X (↑j : ι)))
        f) =
    f

Tactic:
ext j
-- 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 : i_1 ≤ j_1
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : PartialOrder ι
inst_2 : DecidableEq ι
f : piLT X i × X i
j : (↑(Iio i) : Type u_6)
⊢ ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
            ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
              piLT X i × X i))
          ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
              (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
                else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
                X (↑j : ι)))
            f)).1
      j =
    f.1 j

Tactic:
dif_neg j.2.ne

Premises used: dif_neg, dite, LT.lt.ne, 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 : PartialOrder ι
inst_2 : DecidableEq ι
f : piLT X i × X i
⊢ ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
          ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
              f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
            piLT X i × X i))
        ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
            (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
              else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
              X (↑j : ι)))
          f)).2 =
    f.2

Tactic:
dif_pos rfl

Premises used: dif_pos, dite, rfl
-- 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 : i_1 ≤ j_1
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : PartialOrder ι
inst_2 : DecidableEq ι
f : piLT X i × X i
j : (↑(Iio i) : Type u_6)
⊢ ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
            ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
              piLT X i × X i))
          ((fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
              (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
                else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
                X (↑j : ι)))
            f)).1
      j =
    f.1 j

Tactic:
exacts [dif_neg j.2.ne, dif_pos rfl]

Premises used: dif_pos, dif_neg, rfl, LT.lt.ne, 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 : PartialOrder ι
inst_2 : DecidableEq ι
f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)
⊢ (fun (f : piLT X i × X i) (j : (↑(Iic i) : Type u_6)) ↦
        (if h : (↑j : ι) = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ X x) f.2 ⋯
          else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) ⋯) :
          X (↑j : ι)))
      ((fun (f : (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) ↦
          ((fun (j : (↑(Iio i) : Type u_6)) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
              f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯)) :
            piLT X i × X i))
        f) =
    f

Tactic:
grind
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
X : ι → Type u_8
i : ι
inst : PartialOrder ι
inst_1 : DecidableEq ι
f : piLT X i × X i
⊢ (piSplitLE (X := X) : (a : piLT X i × X i) → (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) f
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯) =
    f.2

Tactic:
simp [piSplitLE]

Premises used: InverseSystem.piSplitLE
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
X : ι → Type u_8
i : ι
inst : PartialOrder ι
inst_1 : DecidableEq ι
f : piLT X i × X i
j : ι
hj : j < i
⊢ (piSplitLE (X := X) : (a : piLT X i × X i) → (j : (↑(Iic i) : Type u_6)) → X (↑j : ι)) f
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) j ⋯) =
    f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) j hj)

Tactic:
dif_neg hj.ne

Premises used: dif_neg, dite, LT.lt.ne
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst : LinearOrder ι
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
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ ⋯ : { x : ι // x ∈ Iic i⁺ }) : ι)
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦
            x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ ⋯ : { x : ι // x ∈ Iic i⁺ }) : ι)) i ⋯) :
        ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ ⋯) :
          (a : F (↑⟨i⁺, ⋯⟩ : ι)) → piLT X (↑⟨i⁺, ⋯⟩ : ι))
        x
        (Subtype.mk (p := fun (x : ι) ↦
          x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ ⋯ : { x : ι // x ∈ Iic i⁺ }) : ι)) i ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦
              x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i⁺ ⋯ : { x : ι // x ∈ Iic i⁺ }) : ι)) i ⋯) :
          ι))
    (((e : (a : F i⁺) → F i × X i) x).2 : X i)

Tactic:
simp [piEquivSucc]

Premises used: InverseSystem.piEquivSucc
-- 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
j k : ι
hj : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
⊢ ∀ {j : ι}, j ≤ i → j < i⁺

Tactic:
have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
-- 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
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)
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)
⊢ 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

Premises used: Iff.mp, rfl, Order.le_succ_iff_eq_or_le
-- 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 : 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⁺)
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)
⊢ 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

Premises used: Iff.mp, rfl, Order.le_succ_iff_eq_or_le