awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
zero :
  ∀
    (hj :
      ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
        map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk)
    (hij : 0 ≤ HAdd.hAdd (α := ℕ) 0 1) (hjk : HAdd.hAdd (α := ℕ) 0 1 ≤ k + 1 + 1),
    Eq (α := X 0 ⟶ X (k + 1 + 1))
      (f 0 ≫
        CategoryStruct.comp (Y := X (HAdd.hAdd (α := ℕ) 0 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 0 ⋯)
          (map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯))
      (map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯)
zero₁ :
  ∀ (j : ℕ)
    (hj :
      ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j + 1) (hjk : j + 1 ≤ k),
        map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk)
    (hij : 0 ≤ j + 1 + 1) (hjk : j + 1 + 1 ≤ k + 1 + 1),
    Eq (α := X 0 ⟶ X (k + 1 + 1))
      (f 0 ≫
        CategoryStruct.comp (Y := X (j + 1 + 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 (j + 1) ⋯)
          (map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) ⋯))
      (map f 0 (j + 1 + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) ⋯)
⊢ Eq (α := X 0 ⟶ X (k + 1 + 1))
    (f 0 ≫
      CategoryStruct.comp (Y := X (j + 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 j ⋯)
        (map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯))
    (map f 0 (j + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯)

Tactic:
obtain _ | j := j
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ HAdd.hAdd (α := ℕ) 0 1
hjk : HAdd.hAdd (α := ℕ) 0 1 ≤ k + 1 + 1
⊢ Eq (α := X 0 ⟶ X (k + 1 + 1))
    (f 0 ≫
      CategoryStruct.comp (Y := X (HAdd.hAdd (α := ℕ) 0 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 0 ⋯)
        (map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯))
    (map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯)

Tactic:
simp [map]

Premises used: CategoryTheory.Functor.OfSequence.map
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j + 1) (hjk : j + 1 ≤ k),
    map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk
hij : 0 ≤ j + 1 + 1
hjk : j + 1 + 1 ≤ k + 1 + 1
⊢ Eq (α := X 0 ⟶ X (k + 1 + 1))
    (f 0 ≫
      CategoryStruct.comp (Y := X (j + 1 + 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 (j + 1) ⋯)
        (map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) ⋯))
    (map f 0 (j + 1 + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) ⋯)

Tactic:
simp [map]

Premises used: CategoryTheory.Functor.OfSequence.map
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j k : ℕ
hij : 0 ≤ j
hjk : j ≤ k
zero :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
zero₁ :
  ∀ (j : ℕ)
    (hj :
      ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
        map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk)
    {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j + 1) (hjk : j + 1 ≤ k),
    map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk
⊢ map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Tactic:
induction j generalizing X k with
      | zero =>
          rw [map_id, id_comp]
      | succ j hj =>
          obtain (_ | _ | k) := k
          · lia
          · obtain rfl : j = 0 := by lia
            rw [map_id, comp_id]
          · simp only [map, Nat.reduceAdd]
            rw [hj (fun n ↦ f (n + 1)) (k + 1) (by lia) (by lia)]
            obtain _ | j := j
            all_goals simp [map]

Premises used: CategoryTheory.Functor.OfSequence.map, Nat.reduceAdd, CategoryTheory.Category.comp_id, CategoryTheory.Functor.OfSequence.map_id, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j k : ℕ
hij : i + 1 ≤ j
hjk : j ≤ k
succ : ∀ (hij : i + 1 ≤ 0) (hjk : LE.le (α := ℕ) 0 0), map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk
succ₁ :
  ∀ (hij : i + 1 ≤ 0) (k : ℕ) (hjk : 0 ≤ k + 1), map f (i + 1) (k + 1) ⋯ = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk
succ₂ :
  ∀ (j : ℕ) (hij : i + 1 ≤ j + 1) (hjk : j + 1 ≤ 0), map f (i + 1) 0 ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) 0 hjk
succ₃ :
  ∀ (j : ℕ) (hij : i + 1 ≤ j + 1) (k : ℕ) (hjk : j + 1 ≤ k + 1),
    map f (i + 1) (k + 1) ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) (k + 1) hjk
⊢ map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk

Tactic:
rcases j, k with ⟨(_ | j), (_ | k)⟩
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : i + 1 ≤ 0
hjk : LE.le (α := ℕ) 0 0
⊢ map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : i + 1 ≤ 0
k : ℕ
hjk : 0 ≤ k + 1
⊢ map f (i + 1) (k + 1) ⋯ = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
hjk : j + 1 ≤ 0
⊢ map f (i + 1) 0 ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) 0 hjk

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1
⊢ i ≤ j

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1
⊢ j ≤ k

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1
⊢ map f (i + 1) (k + 1) ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) (k + 1) hjk

Tactic:
exact hi _ j k (by lia) (by lia)
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j k : ℕ
hij : i ≤ j
hjk : j ≤ k
zero :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
        map f i k ⋯ = map f i j hij ≫ map f j k hjk)
    {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i + 1 ≤ j) (hjk : j ≤ k),
    map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk

Tactic:
induction i generalizing X j k with
  | zero =>
      induction j generalizing X k with
      | zero =>
          rw [map_id, id_comp]
      | succ j hj =>
          obtain (_ | _ | k) := k
          · lia
          · obtain rfl : j = 0 := by lia
            rw [map_id, comp_id]
          · simp only [map, Nat.reduceAdd]
            rw [hj (fun n ↦ f (n + 1)) (k + 1) (by lia) (by lia)]
            obtain _ | j := j
            all_goals simp [map]
  | succ i hi =>
      rcases j, k with ⟨(_ | j), (_ | k)⟩
      · lia
      · lia
      · lia
      · exact hi _ j k (by lia) (by lia)

Premises used: CategoryTheory.Functor.OfSequence.map, Nat.reduceAdd, CategoryTheory.Category.comp_id, CategoryTheory.Functor.OfSequence.map_id, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ LE.le (α := ℕ) 5 5

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f 5 5 _example._proof_1 = 𝟙 (X 5)

Tactic:
rfl

Premises used: CategoryTheory.Functor.OfSequence.map, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ LE.le (α := ℕ) 0 3

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f 0 3 _example._proof_1 = f 0 ≫ f 1 ≫ f 2

Tactic:
rfl

Premises used: CategoryTheory.Functor.OfSequence.map, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ LE.le (α := ℕ) 3 7

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f 3 7 _example._proof_1 = f 3 ≫ f 4 ≫ f 5 ≫ f 6

Tactic:
rfl

Premises used: CategoryTheory.Functor.OfSequence.map, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
n : ℕ
⊢ (ofSequence f).map (homOfLE ⋯) = f n

Tactic:
OfSequence.map_le_succ f n

Premises used: CategoryTheory.Functor.OfSequence.map_le_succ
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j : ℕ
φ : i ⟶ j
obtain : ∀ (k : ℕ) (hk : j = i + k), F.map φ ≫ app j = app i ≫ G.map φ
⊢ F.map φ ≫ app j = app i ≫ G.map φ

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le (leOfHom φ)

Premises used: Nat.exists_eq_add_of_le, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j : ℕ
φ : i ⟶ j
k : ℕ
hk : j = i + k
⊢ i ≤ j

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j : ℕ
φ : i ⟶ j
k : ℕ
hk : j = i + k
obtain : F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
⊢ F.map φ ≫ app j = app i ≫ G.map φ

Tactic:
obtain rfl := Subsingleton.elim φ (homOfLE (by lia))

Premises used: CategoryTheory.homOfLE, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j k : ℕ
hk : j = i + k
revert : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)

Tactic:
revert i j
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j : ℕ
hk : j = i + 0
⊢ j = i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
i j : ℕ
hk : j = i + 0
zero : ∀ (hk : j = j + 0), F.map (homOfLE ⋯) ≫ app j = app j ≫ G.map (homOfLE ⋯)
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)

Tactic:
obtain rfl : j = i := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
j : ℕ
hk : j = j + 0
⊢ F.map (homOfLE ⋯) ≫ app j = app j ≫ G.map (homOfLE ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
i j : ℕ
hk' : j = i + (k + 1)
⊢ j = i + k + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
i j : ℕ
hk' : j = i + (k + 1)
succ : ∀ (hk' : i + k + 1 = i + (k + 1)), F.map (homOfLE ⋯) ≫ app (i + k + 1) = app i ≫ G.map (homOfLE ⋯)
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)

Tactic:
obtain rfl : j = i + k + 1 := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
i : ℕ
hk' : i + k + 1 = i + (k + 1)
⊢ i ≤ i + k

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
i : ℕ
hk' : i + k + 1 = i + (k + 1)
⊢ i + k ≤ i + k + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
i : ℕ
hk' : i + k + 1 = i + (k + 1)
⊢ F.map (homOfLE ⋯) ≫ app (i + k + 1) = app i ≫ G.map (homOfLE ⋯)

Tactic:
simp only [← homOfLE_comp (show i ≤ i + k by lia) (show i + k ≤ i + k + 1 by lia),
          Functor.map_comp, assoc, naturality, reassoc_of% (hk rfl)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), Eq (α := F.obj n ⟶ G.obj (n + 1)) (F.map (homOfLE ⋯) ≫ app (n + 1)) (app n ≫ G.map (homOfLE ⋯))
k : ℕ
zero : ∀ ⦃i j : ℕ⦄ (hk : j = i + 0), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
succ :
  ∀ (k : ℕ) (hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)) ⦃i j : ℕ⦄
    (hk : j = i + (k + 1)), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
⊢ ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)

Tactic:
induction k with
    | zero =>
        intro i j hk
        obtain rfl : j = i := by lia
        simp
    | succ k hk =>
        intro i j hk'
        obtain rfl : j = i + k + 1 := by lia
        simp only [← homOfLE_comp (show i ≤ i + k by lia) (show i + k ≤ i + k + 1 by lia),
          Functor.map_comp, assoc, naturality, reassoc_of% (hk rfl)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ LE.le (α := ℕ) 5 5

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ (ofOpSequence f).map (Quiver.Hom.op (homOfLE ⋯)) = 𝟙 ((ofOpSequence f).obj (Opposite.op 5))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ LE.le (α := ℕ) 0 3

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ Eq (α := (ofOpSequence f).obj (Opposite.op 3) ⟶ (ofOpSequence f).obj (Opposite.op 0))
    ((ofOpSequence f).map (Quiver.Hom.op (homOfLE ⋯))) ((f 2 ≫ f 1) ≫ f 0)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ LE.le (α := ℕ) 3 7

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
⊢ Eq (α := (ofOpSequence f).obj (Opposite.op 7) ⟶ (ofOpSequence f).obj (Opposite.op 3))
    ((ofOpSequence f).map (Quiver.Hom.op (homOfLE ⋯))) (((f 6 ≫ f 5) ≫ f 4) ≫ f 3)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
n : ℕ
⊢ (ofOpSequence f).map (Quiver.Hom.op (homOfLE ⋯)) = f n

Tactic:
simp [ofOpSequence]

Premises used: CategoryTheory.Functor.ofOpSequence
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕᵒᵖ C
app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)
naturality :
  ∀ (n : ℕ),
    Eq (α := F.obj (Opposite.op (n + 1)) ⟶ G.obj (Opposite.op n)) (F.map (Quiver.Hom.op (homOfLE ⋯)) ≫ app n)
      (app (n + 1) ≫ G.map (Quiver.Hom.op (homOfLE ⋯)))
x x_1 : ℕᵒᵖ
f : x ⟶ x_1
φ : G.rightOp ⟶ F.rightOp := ofSequence (fun (n : ℕ) ↦ (app n).op) ⋯
⊢ F.map f ≫ app (Opposite.unop x_1) = app (Opposite.unop x) ≫ G.map f

Tactic:
Quiver.Hom.op_inj (φ.naturality f.unop).symm

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{0, v_1, 0, u_1} ℕᵒᵖ C
app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)
naturality :
  ∀ (n : ℕ),
    Eq (α := F.obj (Opposite.op (n + 1)) ⟶ G.obj (Opposite.op n)) (F.map (Quiver.Hom.op (homOfLE ⋯)) ≫ app n)
      (app (n + 1) ≫ G.map (Quiver.Hom.op (homOfLE ⋯)))
x x_1 : ℕᵒᵖ
f : x ⟶ x_1
φ : G.rightOp ⟶ F.rightOp := ofSequence (fun (n : ℕ) ↦ (app n).op) ⋯
⊢ F.map f ≫ app (Opposite.unop x_1) = app (Opposite.unop x) ≫ G.map f

Tactic:
exact Quiver.Hom.op_inj (φ.naturality f.unop).symm

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Balanced.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.ReflectsMonomorphisms
inst_4 : F.ReflectsEpimorphisms
A B : C
f : A ⟶ B
hf : IsIso (F.map f)
⊢ Epi f

Tactic:
haveI : Epi f := epi_of_epi_map F inferInstance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Balanced.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.ReflectsMonomorphisms
inst_4 : F.ReflectsEpimorphisms
A B : C
f : A ⟶ B
hf : IsIso (F.map f)
this : Epi f
⊢ Mono f

Tactic:
haveI : Mono f := mono_of_mono_map F inferInstance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Balanced.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.ReflectsMonomorphisms
inst_4 : F.ReflectsEpimorphisms
A B : C
f : A ⟶ B
hf : IsIso (F.map f)
this_1 : Epi f
this : Mono f
⊢ IsIso f

Tactic:
isIso_of_mono_of_epi f

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Balanced.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.ReflectsMonomorphisms
inst_4 : F.ReflectsEpimorphisms
A B : C
f : A ⟶ B
hf : IsIso (F.map f)
this_1 : Epi f
this : Mono f
⊢ IsIso f

Tactic:
exact isIso_of_mono_of_epi f

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsIsomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : F.PreservesMonomorphisms
inst_5 : Balanced.{v_2, u_2} D
X Y : C
f : X ⟶ Y
h : Mono f
h_1 : Epi f
rw : IsIso (F.map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso (F := F)]

Premises used: CategoryTheory.isIso_iff_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsIsomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : F.PreservesMonomorphisms
inst_5 : Balanced.{v_2, u_2} D
X Y : C
f : X ⟶ Y
h : Mono f
h_1 : Epi f
⊢ IsIso (F.map f)

Tactic:
isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsIsomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : F.PreservesMonomorphisms
inst_5 : Balanced.{v_2, u_2} D
X Y : C
f : X ⟶ Y
h : Mono f
h_1 : Epi f
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi