awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirectedInverseSystem
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
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h : (a : F₂ i) → F₂ j) (ih i x) = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x)
z : DirectLimit F₁ (T := T₁) f₁
j k : ι
h : j ≤ k
x : 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) : F₂ i)
    ((f₂ k i hki : (a : F₂ k) → F₂ i) (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x)) : F₂ i)
simp_rw₂ :
  ih i ((f₁ j i hji : (a : F₁ j) → F₁ i) x) =
    ih i ((f₁ k i hki : (a : F₁ k) → F₁ i) ((f₁ j k h : (a : F₁ j) → F₁ k) x : F₁ k))
⊢ Eq (α := F₂ i)
    ((f₂ ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) j (ih j x)).fst (β := fun (i : ι) ↦ F₂ i)) i hji :
          (a : F₂ ⟨j, ih j x⟩.fst) → F₂ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) j (ih j x)).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))).fst (β := fun (i : ι) ↦
              F₂ i))
            i hki :
          (a : F₂ ⟨k, ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x)⟩.fst) → F₂ i)
        ((Sigma.mk (β := fun (i : ι) ↦ F₂ i) k (ih k ((f₁ j k h : (a : F₁ j) → F₁ k) x))).snd (β := fun (i : ι) ↦
          F₂ i)) :
      F₂ i)

Tactic:
simp_rw [compat, map_map']

Premises used: DirectedSystem.map_map'
-- Module: Mathlib.Order.DirectedInverseSystem
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 ι
ih : (i : ι) → F₁ i → F₂ i
compat :
  ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h : (a : F₂ i) → F₂ j) (ih i x) = ih j ((f₁ i j h : (a : F₁ i) → F₁ j) x)
x : (i : ι) × F₁ i
⊢ Eq (α := DirectLimit F₂ (T := T₂) f₂) (map (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat ⟦x⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ F₂ i) (x.fst (β := fun (i : ι) ↦ F₁ i))
        (ih (x.fst (β := fun (i : ι) ↦ F₁ i)) (x.snd (β := fun (i : ι) ↦ F₁ i)))⟧

Tactic:
rfl

Premises used: DirectLimit.map, DirectLimit.lift, rfl
-- Module: Mathlib.Order.DirectedInverseSystem
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
choose :
  (j : ι) →
    (hzj : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ j) →
      (hwj : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ j) →
        { x : C //
          ∀ (i : ι) (hzi : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ i) (hwi : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ i),
            x =
              ih i
                ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) i hzi : (a : F₁ z.fst) → F₁ i) (z.snd (β := fun (i : ι) ↦ F₁ i)))
                ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) i hwi : (a : F₂ w.fst) → F₂ i)
                  (w.snd (β := fun (i : ι) ↦ F₂ i))) }
⊢ { x : C //
    ∀ (i : ι) (hzi : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ i) (hwi : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ i),
      x =
        ih i ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) i hzi : (a : F₁ z.fst) → F₁ i) (z.snd (β := fun (i : ι) ↦ F₁ i)))
          ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) i hwi : (a : F₂ w.fst) → F₂ i) (w.snd (β := fun (i : ι) ↦ F₂ i))) }

Tactic:
choose j hzj hwj using exists_ge_ge z.1 w.1

Premises used: Sigma.fst, exists_ge_ge
-- Module: Mathlib.Order.DirectedInverseSystem
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
refine :
  ∀ (k : ι) (hzk : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ k) (hwk : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ k),
    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)))
⊢ { x : C //
    ∀ (i : ι) (hzi : z.fst (β := fun (i : ι) ↦ F₁ i) ≤ i) (hwi : w.fst (β := fun (i : ι) ↦ F₂ i) ≤ i),
      x =
        ih i ((f₁ (z.fst (β := fun (i : ι) ↦ F₁ i)) i hzi : (a : F₁ z.fst) → F₁ i) (z.snd (β := fun (i : ι) ↦ F₁ i)))
          ((f₂ (w.fst (β := fun (i : ι) ↦ F₂ i)) i hwi : (a : F₂ w.fst) → F₂ i) (w.snd (β := fun (i : ι) ↦ F₂ i))) }

Tactic:
refine ⟨ih j (f₁ _ _ hzj z.2) (f₂ _ _ hwj w.2), fun k hzk hwk ↦ ?_⟩
-- Module: Mathlib.Order.DirectedInverseSystem
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
have :
  ∀ (i : ι) (hji : j ≤ i) (hki : k ≤ 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)))
⊢ 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)))

Tactic:
have ⟨i, hji, hki⟩ := exists_ge_ge j k
-- Module: Mathlib.Order.DirectedInverseSystem
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)))
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))
⊢ 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)))

Tactic:
simp_rw [compat _ _ hji, compat _ _ hki, map_map']

Premises used: DirectedSystem.map_map'
-- Module: Mathlib.Order.DirectedInverseSystem
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)
x : (i : ι) × F₁ i
y : (i : ι) × F₂ i
i : ι
hxi : x.fst (β := fun (i : ι) ↦ F₁ i) ≤ i
hyi : y.fst (β := fun (i : ι) ↦ F₂ i) ≤ i
⊢ DirectLimit.lift₂ (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat ⟦x⟧ ⟦y⟧ =
    ih i ((f₁ (x.fst (β := fun (i : ι) ↦ F₁ i)) i hxi : (a : F₁ x.fst) → F₁ i) (x.snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ (y.fst (β := fun (i : ι) ↦ F₂ i)) i hyi : (a : F₂ y.fst) → F₂ i) (y.snd (β := fun (i : ι) ↦ F₂ i)))

Tactic:
(lift₂Aux _ _ _ compat _ _).2 ..

Premises used: Quotient.hrecOn₂, Quot.hrecOn₂, DirectLimit.lift₂, Subtype.property, _private.0.DirectLimit.lift₂Aux
-- Module: Mathlib.Order.DirectedInverseSystem
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
rw₂ 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
⊢ 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

Tactic:
rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']

Premises used: DirectLimit.lift₂_def₂, DirectedSystem.map_self'
-- Module: Mathlib.Order.DirectedInverseSystem
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)
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))
⊢ 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)

Tactic:
simp_rw [compat, map_map']

Premises used: DirectedSystem.map_map'
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
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)
x : (i : ι) × F₁ i
y : (i : ι) × F₂ i
i : ι
hxi : x.fst (β := fun (i : ι) ↦ F₁ i) ≤ i
hyi : y.fst (β := fun (i : ι) ↦ F₂ i) ≤ i
⊢ Eq (α := DirectLimit F (T := T) f)
    (map₂ (F₁ := F₁) (F₂ := F₂) (F := F) (T₁ := T₁) f₁ (T₂ := T₂) f₂ (T := T) f ih compat ⟦x⟧ ⟦y⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i
        (ih i ((f₁ (x.fst (β := fun (i : ι) ↦ F₁ i)) i hxi : (a : F₁ x.fst) → F₁ i) (x.snd (β := fun (i : ι) ↦ F₁ i)))
          ((f₂ (y.fst (β := fun (i : ι) ↦ F₂ i)) i hyi : (a : F₂ y.fst) → F₂ i) (y.snd (β := fun (i : ι) ↦ F₂ i))))⟧

Tactic:
lift₂_def₂ ..

Premises used: DirectLimit.lift₂_def₂, DirectLimit.map₂
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
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)
i : ι
x : F₁ i
y : F₂ i
⊢ Eq (α := DirectLimit F (T := T) f)
    (map₂ (F₁ := F₁) (F₂ := F₂) (F := F) (T₁ := T₁) 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⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i (ih i x y)⟧

Tactic:
lift₂_def ..

Premises used: DirectLimit.lift₂_def, DirectLimit.map₂
-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
X : ι → Type u_5
i j : ι
h : i ≤ j
l : (↑(Iio j) : Type u_1)
f : piLT X j
hl : (↑l : ι) < i
⊢ f l = piLTProj (X := X) h f (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑l : ι) hl)

Tactic:
rfl

Premises used: rfl