awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p q : ι
h : p = q
⊢ K.X p = K.X q
have rw : K.X q = K.X q
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
have dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry)
Tactic: dsimp [XIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
have dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry)
Tactic: dsimp [XIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
have dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry)
Tactic: dsimp [XIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
have dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry)
Tactic: dsimp [XIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃
have subst : (K.XIsoOfEq sorry).hom ≫ K.d p₁ p₃ = K.d p₁ p₃
Tactic: subst h
Cleared hypotheses: p₂, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃
have subst : (K.XIsoOfEq sorry).inv ≫ K.d p₂ p₃ = K.d p₂ p₃
Tactic: subst h
Cleared hypotheses: p₁, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃
have subst : K.d p₁ p₂ ≫ (K.XIsoOfEq sorry).hom = K.d p₁ p₂
Tactic: subst h
Cleared hypotheses: p₃, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃
have subst : K.d p₁ p₃ ≫ (K.XIsoOfEq sorry).inv = K.d p₁ p₃
Tactic: subst h
Cleared hypotheses: p₂, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ (ComplexShape.down ℕ).next 0 = 0
have refine : ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
Tactic: refine dif_neg ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
have push : ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ (ComplexShape.down ℕ).next 0 = 0
have refine : ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
Tactic: classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
⊢ (ComplexShape.down ℕ).next 0 = 0
have refine₁ : ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j
Tactic: classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ (ComplexShape.up ℕ).prev 0 = 0
have refine : ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
Tactic: refine dif_neg ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
have push : ∀ (j : ℕ), ¬(ComplexShape.up ℕ).Rel j 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
⊢ (ComplexShape.up ℕ).prev 0 = 0
have refine : ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
Tactic: classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
⊢ (ComplexShape.up ℕ).prev 0 = 0
have refine₁ : ∀ (j : ℕ), ¬(ComplexShape.up ℕ).Rel j 0
Tactic: classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have pos : ∀ (hij : c.Rel i j), f.f i ≫ B.d i j = A.d i j ≫ f.f j
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
pos : ∀ (hij : c.Rel i j), f.f i ≫ B.d i j = A.d i j ≫ f.f j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have neg : ∀ (hij : ¬c.Rel i j), f.f i ≫ B.d i j = A.d i j ≫ f.f j
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have neg : f.f i ≫ B.d i j = 0 ≫ f.f j
Tactic: rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
neg : f.f i ≫ B.d i j = 0 ≫ f.f j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have neg₁ : f.f i ≫ 0 = 0 ≫ f.f j
Tactic: rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
neg : f.f i ≫ B.d i j = 0 ≫ f.f j
neg₁ : f.f i ≫ 0 = 0 ≫ f.f j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have neg₂ : Eq (α := A.X i ⟶ B.X j) 0 (0 ≫ f.f j)
Tactic: rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
neg : f.f i ≫ B.d i j = 0 ≫ f.f j
neg₁ : f.f i ≫ 0 = 0 ≫ f.f j
neg₂ : Eq (α := A.X i ⟶ B.X j) 0 (0 ≫ f.f j)
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j
have neg₃ : Eq.{v + 1} (α := A.X i ⟶ B.X j) 0 0
Tactic: rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f = g
have f₁ : f.f = g.f
Tactic: apply Hom.ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
h : C₁ = C₂
n : ι
⊢ Hom.f (eqToHom h) n = eqToHom ⋯
have subst : Hom.f (eqToHom sorry) n = eqToHom sorry
Tactic: subst h
Cleared hypotheses: C₂, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
⊢ IsZero (C := HomologicalComplex.{v, u, u_1} V c) zero
have refine_1 : ∀ (X : HomologicalComplex.{v, u, u_1} V c) (f : zero ⟶ X), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
refine_1 : ∀ (X : HomologicalComplex.{v, u, u_1} V c) (f : zero ⟶ X), f = default
⊢ IsZero (C := HomologicalComplex.{v, u, u_1} V c) zero
have refine_2 : ∀ (X : HomologicalComplex.{v, u, u_1} V c) (f : X ⟶ zero), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : zero ⟶ X
⊢ f = default
have refine_1 : ∀ (i : ι), f.f i = Hom.f default i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : zero ⟶ X
i : ι
⊢ f.f i = Hom.f default i
have refine_1 : f.f i = Hom.f 0 i
Tactic: dsimp only [zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : X ⟶ zero
⊢ f = default
have refine_2 : ∀ (i : ι), f.f i = Hom.f default i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : X ⟶ zero
i : ι
⊢ f.f i = Hom.f default i
have refine_2 : f.f i = Hom.f 0 i
Tactic: dsimp only [zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
⊢ g = h
have h₁ : ∀ (i : ι), g.f i = h.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i = h.f i
have h₁ : g.f i ≫ φ.f i = h.f i ≫ φ.f i
Tactic: rw [← cancel_mono (φ.f i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
⊢ g = h
have h₁ : ∀ (i : ι), g.f i = h.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i
have h₁ : φ.f i ≫ g.f i = φ.f i ≫ h.f i
Tactic: rw [← cancel_epi (φ.f i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C X Y : HomologicalComplex.{v, u, u_1} V c
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (forget V c) X ⟶ Functor.obj (forget V c) Y) (CategoryTheory.Functor.map (forget V c) a₁)
    (CategoryTheory.Functor.map (forget V c) a₂)
⊢ a₁ = a₂
have h₁ : ∀ (i : ι), a₁.f i = a₂.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'
have subst : φ.f n ≫ (L.XIsoOfEq sorry).hom = (K.XIsoOfEq sorry).hom ≫ φ.f n
Tactic: subst h
Cleared hypotheses: n', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n
have subst : φ.f n ≫ (L.XIsoOfEq sorry).inv = (K.XIsoOfEq sorry).inv ≫ φ.f n
Tactic: subst h
Cleared hypotheses: n', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j j' : ι
rij : c.Rel i j
rij' : c.Rel i j'
⊢ C.d i j' ≫ eqToHom ⋯ = C.d i j
have obtain : ∀ (rij' : c.Rel i j), C.d i j ≫ eqToHom sorry = C.d i j
Tactic: obtain rfl := c.next_eq rij rij'
Cleared hypotheses: j', rij'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i i' j : ι
rij : c.Rel i j
rij' : c.Rel i' j
⊢ eqToHom ⋯ ≫ C.d i' j = C.d i j
have obtain : ∀ (rij' : c.Rel i j), eqToHom sorry ≫ C.d i j = C.d i j
Tactic: obtain rfl := c.prev_eq rij rij'
Cleared hypotheses: i', rij'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j) = kernelSubobject (C.d i j')
have rw : kernelSubobject (C.d i j' ≫ eqToHom sorry) = kernelSubobject (C.d i j')
Tactic: rw [← d_comp_eqToHom C r r']
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
⊢ imageSubobject (C.d i j) = imageSubobject (C.d i' j)
have rw : imageSubobject (eqToHom sorry ≫ C.d i' j) = imageSubobject (C.d i' j)
Tactic: rw [← eqToHom_comp_d C r r']
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ C.xPrev j = C.X i
have rw : C.xPrev j = C.X (c.prev j)
Tactic: rw [← c.prev_eq' r]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ (if h : ∃ (j_1 : ι), c.Rel j_1 j then h.choose (p := fun (a : ι) ↦ c.Rel a j) else j) = j
have hnc : ¬∃ (j_1 : ι), c.Rel j_1 j
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ ¬∃ (j_1 : ι), c.Rel j_1 j
have hnc : ∀ (j_1 : ι), ¬c.Rel j_1 j
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
⊢ False
have this : c.prev j = i
Tactic: have : c.prev j = i := c.prev_eq' hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
this : c.prev j = i
⊢ False
have h₁ : ¬c.Rel i j
Tactic: rw [this] at h
Cleared hypotheses: h, hi, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ C.xNext i = C.X j
have rw : C.xNext i = C.X (c.next i)
Tactic: rw [← c.next_eq' r]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i) = i
have hnc : ¬∃ (j : ι), c.Rel i j
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
⊢ False
have this : c.next i = j
Tactic: have : c.next i = j := c.next_eq' hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
⊢ False
have h₁ : ¬c.Rel i j
Tactic: rw [this] at h
Cleared hypotheses: h, hj, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j
have obtain : ∀ (r : c.Rel (c.prev j) j), C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j
Tactic: obtain rfl := c.prev_eq' r
Cleared hypotheses: i, r
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i = C.d i j ≫ (C.xNextIso r).inv
have obtain : ∀ (r : c.Rel i (c.next i)), C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv
Tactic: obtain rfl := c.next_eq' r
Cleared hypotheses: j, r
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)
have rw : kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)
Tactic: rw [C.dFrom_eq r]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i j : ι
r : c.Rel i j
⊢ imageSubobject (C.dTo j) = imageSubobject (C.d i j)
have rw : imageSubobject ((C.xPrevIso r).hom ≫ C.d i j) = imageSubobject (C.d i j)
Tactic: rw [C.dTo_eq r]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv
have rw : (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv
Tactic: rw [hf i j hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } = 𝟙 C₁
have h : ∀ (i : ι),
  Hom.f ({ f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := sorry }) i =
    Hom.f (𝟙 C₁) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } = 𝟙 C₂
have h : ∀ (i : ι),
  Hom.f ({ f := fun (i : ι) ↦ (f i).inv, comm' := sorry } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ }) i =
    Hom.f (𝟙 C₂) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f hf) i = f i
have w : (isoApp (isoOfComponents f hf) i).hom = (f i).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv
have obtain : ∀ (w : c.Rel (c.prev j) j), f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv
Tactic: obtain rfl := c.prev_eq' w
Cleared hypotheses: i, w