awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    ih i x y = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
j : ι
hzj : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ j
hwj : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ j
k : ι
hzk : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ k
hwk : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ k
i : ι
hji : j ≤ i
hki : k ≤ i
simp_rw :
  ih i
      ((f₁ j i hji : (a : F₁ j) → F₁ i)
        ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) j hzj : (a : F₁ z.fst) → F₁ j) (z.snd (β := fun (i : ι) ↦ F₁ i)) : F₁ j))
      ((f₂ j i hji : (a : F₂ j) → F₂ i)
        ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) j hwj : (a : F₂ w.fst) → F₂ j) (w.snd (β := fun (i : ι) ↦ F₂ i)) :
          F₂ j)) =
    ih k ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) k hzk : (a : F₁ z.fst) → F₁ k) (z.snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) k hwk : (a : F₂ w.fst) → F₂ k) (w.snd (β := fun (i : ι) ↦ F₂ i)))
⊢ ih j ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) j hzj : (a : F₁ z.fst) → F₁ j) (z.snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) j hwj : (a : F₂ w.fst) → F₂ j) (w.snd (β := fun (i : ι) ↦ F₂ i))) =
    ih k ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) k hzk : (a : F₁ z.fst) → F₁ k) (z.snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) k hwk : (a : F₂ w.fst) → F₂ k) (w.snd (β := fun (i : ι) ↦ F₂ i)))
have simp_rw₁ : ih i
    ((f₁ j i hji : (a : F₁ j) → F₁ i)
      ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) j hzj : (a : F₁ z.fst) → F₁ j) (z.snd (β := fun (i : ι) ↦ F₁ i)) : F₁ j))
    ((f₂ j i hji : (a : F₂ j) → F₂ i)
      ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) j hwj : (a : F₂ w.fst) → F₂ j) (w.snd (β := fun (i : ι) ↦ F₂ i)) : F₂ j)) =
  ih i
    ((f₁ k i hki : (a : F₁ k) → F₁ i)
      ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) k hzk : (a : F₁ z.fst) → F₁ k) (z.snd (β := fun (i : ι) ↦ F₁ i)) : F₁ k))
    ((f₂ k i hki : (a : F₂ k) → F₂ i)
      ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) k hwk : (a : F₂ w.fst) → F₂ k) (w.snd (β := fun (i : ι) ↦ F₂ i)) : F₂ k))
Tactic: simp_rw [compat _ _ hji, compat _ _ hki, map_map']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
inst_5 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    ih i x y = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
i : ι
x : F₁ i
y : F₂ i
⊢ DirectLimit.lift₂ (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat ⟦Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y⟧ =
    ih i x y
have rw : ih i
    ((f₁ ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).fst (β := fun (i : ι) ↦ F₁ i)) i sorry : (a : F₁ ⟨i, x⟩.fst) → F₁ i)
      ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i)))
    ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).fst (β := fun (i : ι) ↦ F₂ i)) i sorry : (a : F₂ ⟨i, y⟩.fst) → F₂ i)
      ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i))) =
  ih i x y
Tactic: rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
inst_5 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    ih i x y = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
i : ι
x : F₁ i
y : F₂ i
rw :
  ih i
      ((f₁ ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).fst (β := fun (i : ι) ↦ F₁ i)) i ⋯ : (a : F₁ ⟨i, x⟩.fst) → F₁ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).fst (β := fun (i : ι) ↦ F₂ i)) i ⋯ : (a : F₂ ⟨i, y⟩.fst) → F₂ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i))) =
    ih i x y
⊢ DirectLimit.lift₂ (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat ⟦Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y⟧ =
    ih i x y
have rw₁ : ih i ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i))
    ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).fst (β := fun (i : ι) ↦ F₂ i)) i sorry : (a : F₂ ⟨i, y⟩.fst) → F₂ i)
      ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i))) =
  ih i x y
Tactic: rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
inst_5 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    ih i x y = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
i : ι
x : F₁ i
y : F₂ i
rw :
  ih i
      ((f₁ ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).fst (β := fun (i : ι) ↦ F₁ i)) i ⋯ : (a : F₁ ⟨i, x⟩.fst) → F₁ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).fst (β := fun (i : ι) ↦ F₂ i)) i ⋯ : (a : F₂ ⟨i, y⟩.fst) → F₂ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i))) =
    ih i x y
rw₁ :
  ih i ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i))
      ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).fst (β := fun (i : ι) ↦ F₂ i)) i ⋯ : (a : F₂ ⟨i, y⟩.fst) → F₂ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i))) =
    ih i x y
⊢ DirectLimit.lift₂ (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat ⟦Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y⟧ =
    ih i x y
have rw₂ : ih i ((Sigma.mk (β := fun (i : ι) ↦ F₁ i) i x).snd (β := fun (i : ι) ↦ F₁ i))
    ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) i y).snd (β := fun (i : ι) ↦ F₂ i)) =
  ih i x y
Tactic: rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
ih : (i : ι) → F₁ i → F₂ i → F i
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    (f i j h : (a : F i) → F j) (ih i x y) = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
j k : ι
h : j ≤ k
x : F₁ j
y : F₂ j
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ Eq (α := F i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ F i) j (ih j x y)).fst (β := fun (i : ι) ↦ F i)) i hji :
          (a : F ⟨j, ih j x y⟩.fst) → F i)
        ((Sigma.mk (β := fun (i : ι) ↦ F i) j (ih j x y)).snd (β := fun (i : ι) ↦ F i)) :
      F i)
    ((f
            ((Sigma.mk (β := fun (i : ι) ↦ F i) k
                  (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y))).fst
              (β := fun (i : ι) ↦ F i))
            i hki :
          (a : F ⟨k, ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y)⟩.fst) → F i)
        ((Sigma.mk (β := fun (i : ι) ↦ F i) k
              (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y))).snd
          (β := fun (i : ι) ↦ F i)) :
      F i)
have simp_rw : Eq (α := F i) ((f j i hji : (a : F j) → F i) (ih j x y) : F i)
  ((f k i hki : (a : F k) → F i) (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y)) : F i)
Tactic: simp_rw [compat, map_map']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
ih : (i : ι) → F₁ i → F₂ i → F i
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
    (f i j h : (a : F i) → F j) (ih i x y) = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
j k : ι
h : j ≤ k
x : F₁ j
y : F₂ j
i : ι
hji : j ≤ i
hki : k ≤ i
simp_rw simp_rw₁ :
  Eq (α := F i) ((f j i hji : (a : F j) → F i) (ih j x y) : F i)
    ((f k i hki : (a : F k) → F i) (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y)) : F i)
⊢ Eq (α := F i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ F i) j (ih j x y)).fst (β := fun (i : ι) ↦ F i)) i hji :
          (a : F ⟨j, ih j x y⟩.fst) → F i)
        ((Sigma.mk (β := fun (i : ι) ↦ F i) j (ih j x y)).snd (β := fun (i : ι) ↦ F i)) :
      F i)
    ((f
            ((Sigma.mk (β := fun (i : ι) ↦ F i) k
                  (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y))).fst
              (β := fun (i : ι) ↦ F i))
            i hki :
          (a : F ⟨k, ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y)⟩.fst) → F i)
        ((Sigma.mk (β := fun (i : ι) ↦ F i) k
              (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x) ((f₂ j k h : (a : F₂ j) → F₂ k) y))).snd
          (β := fun (i : ι) ↦ F i)) :
      F i)
have simp_rw₂ : ih i ((f₁ j i hji : (a : F₁ j) → F₁ i) x) ((f₂ j i hji : (a : F₂ j) → F₂ i) y) =
  ih i ((f₁ k i hki : (a : F₁ k) → F₁ i) ((f₁ j k h : (a : F₁ j) → F₁ k) x : F₁ k))
    ((f₂ k i hki : (a : F₂ k) → F₂ i) ((f₂ j k h : (a : F₂ j) → F₂ k) y : F₂ k))
Tactic: simp_rw [compat, map_map']
-- 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 → 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))
⊢ (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
have 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) sorry f) 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 (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 sorry;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry) : ι))
                    (↑l : ι) sorry))
              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: ext j l
-- 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 → 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 ⋯
⊢ (↑((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
have a : ∀ (le : j ≤ Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry),
  (↑((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) sorry f) 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 (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 sorry;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry) : ι))
                    (↑l : ι) sorry))
              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: obtain le | le := le_total j ⟨k, k.2.2⟩
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
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 : ι)
| (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) k (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)
have 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)
Tactic: rw [← (piLTLim hi).right_inv f]
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
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 =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) k
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑k : ι)) (↑l : ι) hl)
have 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)
Tactic: conv_rhs => rw [← (piLTLim hi).right_inv f]
-- 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 : 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) =
    f
have 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 : ι) sorry),
                f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry)) :
              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 sorry
                else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) sorry) :
                X (↑j : ι)))
            f)).1
      j =
    f.1 j
Tactic: ext j
-- 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 : 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
⊢ (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
have 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 : ι) sorry),
            f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry)) :
          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 sorry
            else f.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑j : ι) sorry) :
            X (↑j : ι)))
        f)).2 =
  f.2
Tactic: ext j