awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
have rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
have rw₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
have rw₂ : f.map' 1 2 _proof_8 _proof_25 ≫ 𝟙 (f.obj' 2 _proof_25) = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₂ : f.map' 1 2 _proof_8 _proof_25 ≫ 𝟙 (f.obj' 2 _proof_25) = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
have rw₃ : f.map' 1 2 _proof_8 _proof_25 = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₂ : f.map' 1 2 _proof_8 _proof_25 ≫ 𝟙 (f.obj' 2 _proof_25) = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₃ : f.map' 1 2 _proof_8 _proof_25 = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
have rw₄ : f.map' 1 2 _proof_8 _proof_25 = f.map' 1 2 _proof_8 _proof_25
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
have rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
Tactic: rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id,
      comp_id, app₂.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
have rw₁ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
Tactic: rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id,
      comp_id, app₂.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₁ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
have rw₂ : f.map' 2 3 _proof_25 _proof_26 ≫ 𝟙 (f.obj' 3 _proof_26) = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
Tactic: rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id,
      comp_id, app₂.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₁ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₂ : f.map' 2 3 _proof_25 _proof_26 ≫ 𝟙 (f.obj' 3 _proof_26) = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
have rw₃ : f.map' 2 3 _proof_25 _proof_26 = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
Tactic: rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id,
      comp_id, app₂.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₁ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₂ : f.map' 2 3 _proof_25 _proof_26 ≫ 𝟙 (f.obj' 3 _proof_26) = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₃ : f.map' 2 3 _proof_25 _proof_26 = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
have rw₄ : f.map' 2 3 _proof_25 _proof_26 = f.map' 2 3 _proof_25 _proof_26
Tactic: rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id,
      comp_id, app₂.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
have rw : app.hom ≫ g.map' n (n + 1) sorry h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) sorry h
Tactic: rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
rw : app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
have rw₁ : f.map' n (n + 1) sorry h ≫ app'.hom ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) sorry h
Tactic: rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
rw : app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₁ : f.map' n (n + 1) ⋯ h ≫ app'.hom ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
have rw₂ : f.map' n (n + 1) sorry h ≫ 𝟙 (f.obj' (n + 1) h) = app.hom ≫ app.inv ≫ f.map' n (n + 1) sorry h
Tactic: rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
rw : app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₁ : f.map' n (n + 1) ⋯ h ≫ app'.hom ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₂ : f.map' n (n + 1) ⋯ h ≫ 𝟙 (f.obj' (n + 1) h) = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
have rw₃ : f.map' n (n + 1) sorry h = app.hom ≫ app.inv ≫ f.map' n (n + 1) sorry h
Tactic: rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
rw : app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₁ : f.map' n (n + 1) ⋯ h ≫ app'.hom ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₂ : f.map' n (n + 1) ⋯ h ≫ 𝟙 (f.obj' (n + 1) h) = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₃ : f.map' n (n + 1) ⋯ h = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
have rw₄ : f.map' n (n + 1) sorry h = f.map' n (n + 1) sorry h
Tactic: rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
⊢ g.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_48
have rw : app₀.inv ≫ f.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry sorry = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_48
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
⊢ g.map' 1 2 _proof_8 _proof_49 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_49
have rw : app₁.inv ≫ f.map' 1 (HAdd.hAdd (α := ℕ) 1 1) sorry sorry = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_49
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
⊢ g.map' 2 3 _proof_25 _proof_50 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_50
have rw : app₂.inv ≫ f.map' 2 (HAdd.hAdd (α := ℕ) 2 1) sorry sorry = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_50
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
⊢ g.map' 3 4 _proof_50 _proof_51 ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_51
have rw : app₃.inv ≫ f.map' 3 (HAdd.hAdd (α := ℕ) 3 1) sorry sorry = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_51
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ g.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_84
have rw : app₀.inv ≫ f.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry sorry = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_84
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ g.map' 1 2 _proof_8 _proof_85 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_85
have rw : app₁.inv ≫ f.map' 1 (HAdd.hAdd (α := ℕ) 1 1) sorry sorry = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_85
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ g.map' 2 3 _proof_25 _proof_86 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_86
have rw : app₂.inv ≫ f.map' 2 (HAdd.hAdd (α := ℕ) 2 1) sorry sorry = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_86
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]