awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
⊢ mn + a = a''
have rw₂ : m + n + a = m + (n + a)
Tactic: rw [← ha'', ← ha', ← hnm, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
rw₂ : m + n + a = m + (n + a)
⊢ mn + a = a''
have rw₃ : m + (n + a) = m + (n + a)
Tactic: rw [← ha'', ← ha', ← hnm, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ n + a' = a
have rw : n + (m + a) = a
Tactic: rw [← ha', ← add_assoc, hnm, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : n + (m + a) = a
⊢ n + a' = a
have rw₁ : n + m + a = a
Tactic: rw [← ha', ← add_assoc, hnm, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : n + (m + a) = a
rw₁ : n + m + a = a
⊢ n + a' = a
have rw₂ : 0 + a = a
Tactic: rw [← ha', ← add_assoc, hnm, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : n + (m + a) = a
rw₁ : n + m + a = a
rw₂ : 0 + a = a
⊢ n + a' = a
have rw₃ : a = a
Tactic: rw [← ha', ← add_assoc, hnm, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + n = 0
have rw : m + n + m = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
⊢ m + n = 0
have rw₁ : m + (n + m) = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
⊢ m + n = 0
have rw₂ : m + 0 = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
⊢ m + n = 0
have rw₃ : m + 0 = m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
rw₃ : m + 0 = m
⊢ m + n = 0
have rw₄ : m = m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + n = 0
have rw : m + n + m = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
⊢ m + n = 0
have rw₁ : m + (n + m) = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
⊢ m + n = 0
have rw₂ : m + 0 = 0 + m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
⊢ m + n = 0
have rw₃ : m + 0 = m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
rw₃ : m + 0 = m
⊢ m + n = 0
have rw₄ : m = m
Tactic: rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (hypothesis)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ NatTrans.app (Iso.hom (F.shiftIso n a' a ⋯)) X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map (map (shiftFunctor C n) f ≫ NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) Y)
have hnm' : m + n = 0
Tactic: have hnm' : m + n = 0 := by
    rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a
have rw : a₃ + (a₂ + a₁) = a
Tactic: rw [← h₁₂, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
rw : a₃ + (a₂ + a₁) = a
rw₁ : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a
have rw₂ : a = a
Tactic: rw [← h₁₂, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h rw : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a
have rw₁ : a = a
Tactic: rw [← h₂₃, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ a + m₀ = a
have rw : a + 0 = a
Tactic: rw [hm₀, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
rw : a + 0 = a
⊢ a + m₀ = a
have rw₁ : a = a
Tactic: rw [hm₀, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ comp (mk₀ m₀ hm₀ f) g ⋯ = f ≫ g
have subst : comp (mk₀ 0 sorry f) g sorry = f ≫ g
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ a + m₀ = a
have rw : a + 0 = a
Tactic: rw [hm₀, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
rw : a + 0 = a
⊢ a + m₀ = a
have rw₁ : a = a
Tactic: rw [hm₀, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ m₀ + a = a
have rw : 0 + a = a
Tactic: rw [hm₀, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
rw : 0 + a = a
⊢ m₀ + a = a
have rw₁ : a = a
Tactic: rw [hm₀, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ f.comp (mk₀ m₀ hm₀ g) ⋯ = f ≫ Functor.map (shiftFunctor C a) g
have subst : f.comp (mk₀ 0 sorry g) sorry = f ≫ Functor.map (shiftFunctor C a) g
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ m₀ + a = a
have rw : 0 + a = a
Tactic: rw [hm₀, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
rw : 0 + a = a
⊢ m₀ + a = a
have rw₁ : a = a
Tactic: rw [hm₀, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ c = 0
have rw : b + a = 0
Tactic: rw [← h, ha, hb, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
rw : b + a = 0
⊢ c = 0
have rw₁ : b + 0 = 0
Tactic: rw [← h, ha, hb, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
rw : b + a = 0
rw₁ : b + 0 = 0
⊢ c = 0
have rw₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [← h, ha, hb, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (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
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
rw : b + a = 0
rw₁ : b + 0 = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ c = 0
have rw₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← h, ha, hb, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ Eq (α := ShiftedHom X Z c) (comp (mk₀ a ha f) (mk₀ b hb g) h) (mk₀ c ⋯ (f ≫ g))
have subst : ∀ (h : HAdd.hAdd (α := M) 0 0 = c), Eq (α := ShiftedHom X Z c) (comp (mk₀ 0 sorry f) (mk₀ 0 sorry g) h) (mk₀ c sorry (f ≫ g))
Tactic: subst ha hb
Cleared hypotheses: a, b, h, ha, hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : HAdd.hAdd (α := M) 0 0 = c
⊢ c = 0
have rw : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [← h, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : HAdd.hAdd (α := M) 0 0 = c
rw : HAdd.hAdd (α := M) 0 0 = 0
⊢ c = 0
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← h, zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : HAdd.hAdd (α := M) 0 0 = c
⊢ Eq (α := ShiftedHom X Z c) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ c ⋯ (f ≫ g))
have obtain : ∀ (h : HAdd.hAdd (α := M) 0 0 = 0),
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 sorry f) (mk₀ 0 sorry g) h) (mk₀ 0 sorry (f ≫ g))
Tactic: obtain rfl : c = 0 := by rw [← h, zero_add]
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : HAdd.hAdd (α := M) 0 0 = 0
⊢ Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))
have rw : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ mk₀ 0 sorry g) (mk₀ 0 sorry (f ≫ g))
Tactic: rw [mk₀_comp, mk₀, mk₀, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : HAdd.hAdd (α := M) 0 0 = 0
rw : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ mk₀ 0 ⋯ g) (mk₀ 0 ⋯ (f ≫ g))
⊢ Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))
have rw₁ : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Z)
  (mk₀ 0 sorry (f ≫ g))
Tactic: rw [mk₀_comp, mk₀, mk₀, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : HAdd.hAdd (α := M) 0 0 = 0
rw : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ mk₀ 0 ⋯ g) (mk₀ 0 ⋯ (f ≫ g))
rw₁ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    (mk₀ 0 ⋯ (f ≫ g))
⊢ Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))
have rw₂ : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Z)
  ((f ≫ g) ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Z)
Tactic: rw [mk₀_comp, mk₀, mk₀, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : HAdd.hAdd (α := M) 0 0 = 0
rw : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ mk₀ 0 ⋯ g) (mk₀ 0 ⋯ (f ≫ g))
rw₁ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    (mk₀ 0 ⋯ (f ≫ g))
rw₂ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    ((f ≫ g) ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
⊢ Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))
have rw₃ : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Z)
  (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Z)
Tactic: rw [mk₀_comp, mk₀, mk₀, assoc]