awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ 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) ⋯)
have zero : ∀
  (hj :
    ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
      map f 0 k sorry = 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 sorry)
        (map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) sorry))
    (map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) sorry)
Tactic: obtain _ | j := j
Cleared hypotheses: j, hj, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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) ⋯)
⊢ 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) ⋯)
have 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 sorry = 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) sorry)
        (map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) sorry))
    (map f 0 (j + 1 + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) (j + 1) (k + 1) sorry)
Tactic: obtain _ | j := j
Cleared hypotheses: j, hj, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
have zero : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
  map f 0 k sorry = map f 0 0 hij ≫ map f 0 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]
Cleared hypotheses: X, f, j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
have zero₁ : ∀ (j : ℕ)
  (hj :
    ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
      map f 0 k sorry = 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 sorry = map f 0 (j + 1) hij ≫ map f (j + 1) 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]
Cleared hypotheses: X, f, j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk
have succ : ∀ (hij : i + 1 ≤ 0) (hjk : LE.le (α := ℕ) 0 0), map f (i + 1) 0 sorry = map f (i + 1) 0 hij ≫ map f 0 0 hjk
Tactic: rcases j, k with ⟨(_ | j), (_ | k)⟩
Cleared hypotheses: j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk
have succ₁ : ∀ (hij : i + 1 ≤ 0) (k : ℕ) (hjk : 0 ≤ k + 1), map f (i + 1) (k + 1) sorry = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk
Tactic: rcases j, k with ⟨(_ | j), (_ | k)⟩
Cleared hypotheses: j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk
have succ₂ : ∀ (j : ℕ) (hij : i + 1 ≤ j + 1) (hjk : j + 1 ≤ 0), map f (i + 1) 0 sorry = map f (i + 1) (j + 1) hij ≫ map f (j + 1) 0 hjk
Tactic: rcases j, k with ⟨(_ | j), (_ | k)⟩
Cleared hypotheses: j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk
have succ₃ : ∀ (j : ℕ) (hij : i + 1 ≤ j + 1) (k : ℕ) (hjk : j + 1 ≤ k + 1),
  map f (i + 1) (k + 1) sorry = map f (i + 1) (j + 1) hij ≫ map f (j + 1) (k + 1) hjk
Tactic: rcases j, k with ⟨(_ | j), (_ | k)⟩
Cleared hypotheses: j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk
have zero : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
  map f 0 k sorry = map f 0 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)
Cleared hypotheses: X, f, i, j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk
have succ : ∀ (i : ℕ)
  (hi :
    ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
      map f i k sorry = 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 sorry = map f (i + 1) 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)
Cleared hypotheses: X, f, i, j, k, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ F.map φ ≫ app j = app i ≫ G.map φ
have obtain : ∀ (k : ℕ) (hk : j = i + k), F.map φ ≫ app j = app i ≫ G.map φ
Tactic: obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le (leOfHom φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ F.map φ ≫ app j = app i ≫ G.map φ
have obtain : F.map (homOfLE sorry) ≫ app j = app i ≫ G.map (homOfLE sorry)
Tactic: obtain rfl := Subsingleton.elim φ (homOfLE (by lia))
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
have revert : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE sorry) ≫ app j = app i ≫ G.map (homOfLE sorry)
Tactic: revert i j
Cleared hypotheses: i, j, hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
have zero : ∀ (hk : j = j + 0), F.map (homOfLE sorry) ≫ app j = app j ≫ G.map (homOfLE sorry)
Tactic: obtain rfl : j = i := by lia
Cleared hypotheses: i, hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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)
⊢ F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
have succ : ∀ (hk' : i + k + 1 = i + (k + 1)), F.map (homOfLE sorry) ≫ app (i + k + 1) = app i ≫ G.map (homOfLE sorry)
Tactic: obtain rfl : j = i + k + 1 := by lia
Cleared hypotheses: j, hk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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 : ℕ
⊢ ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
have zero : ∀ ⦃i j : ℕ⦄ (hk : j = i + 0), F.map (homOfLE sorry) ≫ app j = app i ≫ G.map (homOfLE sorry)
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)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.OfSequence (goal)
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 ⋯)
⊢ ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
have succ : ∀ (k : ℕ) (hk : ∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE sorry) ≫ app j = app i ≫ G.map (homOfLE sorry)) ⦃i j : ℕ⦄
  (hk : j = i + (k + 1)), F.map (homOfLE sorry) ≫ app j = app i ≫ G.map (homOfLE sorry)
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)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced (hypothesis)
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)
⊢ IsIso f
have this : Epi f
Tactic: haveI : Epi f := epi_of_epi_map F inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced (hypothesis)
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
⊢ IsIso f
have this₁ : Mono f
Tactic: haveI : Mono f := mono_of_mono_map F inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced (goal)
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
have rw : IsIso (F.map f)
Tactic: rw [← isIso_iff_of_reflects_iso (F := F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
inst_4 : G.ReflectsIsomorphisms
A B : C
f : A ⟶ B
hf : IsIso (G.map (F.map f))
⊢ IsIso f
have this : IsIso (F.map f)
Tactic: haveI := isIso_of_reflects_iso (F.map f) G
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : (F ⋙ G).ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (F.map f)
⊢ IsIso f
have rw : IsIso ((F ⋙ G).map f)
Tactic: rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : (F ⋙ G).ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
have dsimp : IsIso (G.map (F.map f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
⊢ IsIso f
have rw : ∀ (X_1 : C), IsIso (f.app X_1)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
Z : C
⊢ IsIso (f.app Z)
have rw : IsIso (F.map (f.app Z))
Tactic: rw [← isIso_iff_of_reflects_iso _ F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
Z : C
⊢ IsIso (F.map (f.app Z))
have change : IsIso (X := (obj (obj (whiskeringRight C D E) F) X).obj Z) (NatTrans.app (map (obj (whiskeringRight C D E) F) f) Z)
Tactic: change IsIso ((((whiskeringRight C D E).obj F).map f).app Z)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (goal)
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 G : Functor.{v_1, v_2, u_1, u_2} C D
α : F ≅ G
inst_2 : F.ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (G.map f)
⊢ IsIso f
have rw : IsIso (α.hom.app A ≫ G.map f ≫ α.inv.app B)
Tactic: rw [← isIso_iff_of_reflects_iso _ F, ← NatIso.naturality_2 α f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
⊢ IsZero.{v_1, u_1} X ↔ ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
have refine : ∀ (hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)), IsZero.{v_1, u_1} X
Tactic: refine ⟨fun hX _ ↦ Functor.map_isZero _ hX, fun hX ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ IsIso φ
have rw : ∀ (i : I), IsIso ((F i).map φ)
Tactic: rw [hP.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ IsZero.{v_1, u_1} X
have this : IsIso φ
Tactic: have : IsIso φ := by
    rw [hP.isIso_iff]
    exact fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ S.Exact ↔ ∀ (i : I), ShortComplex.Exact (S.map (F i))
have refine : ∀ (hS : ∀ (i : I), ShortComplex.Exact (S.map (F i))), S.Exact
Tactic: refine ⟨fun hS i ↦ hS.map _, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.Exact (S.map (F i))
⊢ S.Exact
have simp : ∀ (hS : ∀ (i : I), IsZero.{v_2, u_3} (ShortComplex.homology (S.map (F i)))), IsZero.{v_1, u_1} S.homology
Tactic: simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
Cleared hypotheses: hS