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 → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
z : DirectLimit F (T := T) f
x y : (i : ι) × F i
h : x ≈ y
k : ι
hxk : x.fst (β := fun (i : ι) ↦ F i) ≤ k
hyk : y.fst (β := fun (i : ι) ↦ F i) ≤ k
eq :
  Eq (α := F k)
    ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
simp_rw simp_rw₁ :
  @Eq.rec _ _ (fun (x_1 : Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) (x : ⟦x⟧ = x_1) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) ⟦y⟧ ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
⊢ Eq.ndrec (a := ⟦x⟧) (motive := fun (x : DirectLimit F (T := T) f) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) (b := ⟦y⟧) ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
have simp_rw₂ : ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i)) =
  ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
Tactic: simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]
-- 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 → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
z : DirectLimit F (T := T) f
x y : (i : ι) × F i
h : x ≈ y
k : ι
hxk : x.fst (β := fun (i : ι) ↦ F i) ≤ k
hyk : y.fst (β := fun (i : ι) ↦ F i) ≤ k
eq :
  Eq (α := F k)
    ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
simp_rw simp_rw₁ :
  @Eq.rec _ _ (fun (x_1 : Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) (x : ⟦x⟧ = x_1) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) ⟦y⟧ ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₂ :
  ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i)) =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
⊢ Eq.ndrec (a := ⟦x⟧) (motive := fun (x : DirectLimit F (T := T) f) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) (b := ⟦y⟧) ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
have simp_rw₃ : ih k ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i))) =
  ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
Tactic: simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]
-- 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 → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
z : DirectLimit F (T := T) f
x y : (i : ι) × F i
h : x ≈ y
k : ι
hxk : x.fst (β := fun (i : ι) ↦ F i) ≤ k
hyk : y.fst (β := fun (i : ι) ↦ F i) ≤ k
eq :
  Eq (α := F k)
    ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
simp_rw simp_rw₁ :
  @Eq.rec _ _ (fun (x_1 : Quotient (α := (i : ι) × F i) (setoid (F := F) (T := T) f)) (x : ⟦x⟧ = x_1) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) ⟦y⟧ ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₂ :
  ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i)) =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
simp_rw₃ :
  ih k ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i))) =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
⊢ Eq.ndrec (a := ⟦x⟧) (motive := fun (x : DirectLimit F (T := T) f) ↦ C)
      (ih (x.fst (β := fun (i : ι) ↦ F i)) (x.snd (β := fun (i : ι) ↦ F i))) (b := ⟦y⟧) ⋯ =
    ih (y.fst (β := fun (i : ι) ↦ F i)) (y.snd (β := fun (i : ι) ↦ F i))
have simp_rw₄ : ih k ((f (x.fst (β := fun (i : ι) ↦ F i)) k hxk : (a : F x.fst) → F k) (x.snd (β := fun (i : ι) ↦ F i))) =
  ih k ((f (y.fst (β := fun (i : ι) ↦ F i)) k hyk : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)))
Tactic: simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 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)
inst_3 : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h : (a : F i) → F j) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
⊢ Eq (α := DirectLimit F (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
have rw : Eq (α := DirectLimit F (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i y⟧
Tactic: rw [h i eq]
-- 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
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
⊢ 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)
have 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)
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
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)
⊢ 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)
have 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))
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 ι
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
⊢ { 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))) }
have 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))) }
Tactic: choose j hzj hwj using exists_ge_ge z.1 w.1
-- 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
⊢ { 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))) }
have 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)))
Tactic: refine ⟨ih j (f₁ _ _ hzj z.2) (f₂ _ _ hwj w.2), fun k hzk hwk ↦ ?_⟩
-- 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
⊢ 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 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)))
Tactic: have ⟨i, hji, hki⟩ := exists_ge_ge j k
-- 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
⊢ 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 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']