awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
rw : ψ₁.φH ≫ h₂.ι = ψ₂.φH ≫ h₂.ι
rw₁ : h₁.ι ≫ ψ₁.φQ = ψ₂.φH ≫ h₂.ι
rw₂ : h₁.ι ≫ ψ₁.φQ = h₁.ι ≫ ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH
have rw₃ : h₁.ι ≫ ψ₂.φQ = h₁.ι ≫ ψ₂.φQ
Tactic: rw [← cancel_mono h₂.ι, commι, commι, hQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁ = ψ₂
have hH : ψ₁.φH = ψ₂.φH
Tactic: have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂
have mk : ∀ (φQ : h₁.Q ⟶ h₂.Q) (φH : h₁.H ⟶ h₂.H) (commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p) (commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃)
  (commι : φH ≫ h₂.ι = h₁.ι ≫ φQ)
  (hQ :
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ = ψ₂.φQ)
  (hH :
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH),
  { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } = ψ₂
Tactic: cases ψ₁
Cleared hypotheses: ψ₁, hQ, hH
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₂ : RightHomologyMapData φ h₁ h₂
φQ : h₁.Q ⟶ h₂.Q
φH : h₁.H ⟶ h₂.H
commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
commι : φH ≫ h₂.ι = h₁.ι ≫ φQ
hQ : { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ = ψ₂.φQ
hH : { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH
⊢ { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } = ψ₂
have mk : ∀ (φQ_1 : h₁.Q ⟶ h₂.Q) (φH_1 : h₁.H ⟶ h₂.H) (commp_1 : h₁.p ≫ φQ_1 = φ.τ₂ ≫ h₂.p)
  (commg'_1 : φQ_1 ≫ h₂.g' = h₁.g' ≫ φ.τ₃) (commι_1 : φH_1 ≫ h₂.ι = h₁.ι ≫ φQ_1)
  (hQ :
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ =
      { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 :
          RightHomologyMapData φ h₁ h₂ }.φQ)
  (hH :
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH =
      { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 :
          RightHomologyMapData φ h₁ h₂ }.φH),
  { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } =
    { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 }
Tactic: cases ψ₂
Cleared hypotheses: ψ₂, hQ, hH
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ S₁.f ≫ φ.τ₂ ≫ h₂.p = 0
have rw : φ.τ₁ ≫ S₂.f ≫ h₂.p = 0
Tactic: rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : φ.τ₁ ≫ S₂.f ≫ h₂.p = 0
⊢ S₁.f ≫ φ.τ₂ ≫ h₂.p = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ h₂.Q) (φ.τ₁ ≫ 0) 0
Tactic: rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : φ.τ₁ ≫ S₂.f ≫ h₂.p = 0
rw₁ : Eq (α := S₁.X₁ ⟶ h₂.Q) (φ.τ₁ ≫ 0) 0
⊢ S₁.f ≫ φ.τ₂ ≫ h₂.p = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h₂.Q) 0 0
Tactic: rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw₂ : φ.τ₂ ≫ h₂.p ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₂ : φ.τ₂ ≫ h₂.p ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw₃ : φ.τ₂ ≫ S₂.g = h₁.p ≫ h₁.g' ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₂ : φ.τ₂ ≫ h₂.p ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₃ : φ.τ₂ ≫ S₂.g = h₁.p ≫ h₁.g' ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw₄ : S₁.g ≫ φ.τ₃ = h₁.p ≫ h₁.g' ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₂ : φ.τ₂ ≫ h₂.p ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₃ : φ.τ₂ ≫ S₂.g = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₄ : S₁.g ≫ φ.τ₃ = h₁.p ≫ h₁.g' ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
have rw₅ : S₁.g ≫ φ.τ₃ = S₁.g ≫ φ.τ₃
Tactic: rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
⊢ RightHomologyMapData φ h₁ h₂
have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
Tactic: have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
    rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
⊢ (h₁.ι ≫ φQ) ≫ h₂.g' = 0
have rw : h₁.ι ≫ φQ ≫ h₂.g' = 0
Tactic: rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
rw : h₁.ι ≫ φQ ≫ h₂.g' = 0
⊢ (h₁.ι ≫ φQ) ≫ h₂.g' = 0
have rw₁ : h₁.ι ≫ h₁.g' ≫ φ.τ₃ = 0
Tactic: rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
rw : h₁.ι ≫ φQ ≫ h₂.g' = 0
rw₁ : h₁.ι ≫ h₁.g' ≫ φ.τ₃ = 0
⊢ (h₁.ι ≫ φQ) ≫ h₂.g' = 0
have rw₂ : Eq (α := h₁.H ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
rw : h₁.ι ≫ φQ ≫ h₂.g' = 0
rw₁ : h₁.ι ≫ h₁.g' ≫ φ.τ₃ = 0
rw₂ : Eq (α := h₁.H ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ (h₁.ι ≫ φQ) ≫ h₂.g' = 0
have rw₃ : Eq.{v_1 + 1} (α := h₁.H ⟶ S₂.X₃) 0 0
Tactic: rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φH = γ₂.φH
have rw : γ₂.φH = γ₂.φH
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φQ = γ₂.φQ
have rw : γ₂.φQ = γ₂.φQ
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
A : C
f₁ f₂ : A ⟶ S.rightHomology
⊢ f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι
have rw : f₁ = f₂ ↔ f₁ = f₂
Tactic: rw [cancel_mono]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
A : C
f₁ f₂ : S.opcycles ⟶ A
⊢ f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂
have rw : f₁ = f₂ ↔ f₁ = f₂
Tactic: rw [cancel_epi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
hf : S.f = 0
⊢ S.opcycles ≅ S.X₂
have this : IsIso (Y := S.opcycles) S.pOpcycles
Tactic: have := S.isIso_pOpcycles hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
hg : S.g = 0
⊢ S.opcycles ≅ S.rightHomology
have this : IsIso (X := S.rightHomology) S.rightHomologyι
Tactic: have := S.isIso_rightHomologyι hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
have rw : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ rightHomologyMap' φ₂ h₂ h₃
Tactic: rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
    RightHomologyMapData.comp_φH]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ rightHomologyMap' φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
have rw₁ : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
    RightHomologyMapData.comp_φH]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ rightHomologyMap' φ₂ h₂ h₃
rw₁ : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
have rw₂ : (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
    RightHomologyMapData.comp_φH]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ rightHomologyMap' φ₂ h₂ h₃
rw₁ : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
rw₂ : (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
have rw₃ : γ₁.φH ≫ γ₂.φH = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
    RightHomologyMapData.comp_φH]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
have rw : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ opcyclesMap' φ₂ h₂ h₃
Tactic: rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
    RightHomologyMapData.comp_φQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ opcyclesMap' φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
have rw₁ : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ γ₂.φQ
Tactic: rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
    RightHomologyMapData.comp_φQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ opcyclesMap' φ₂ h₂ h₃
rw₁ : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ γ₂.φQ
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
have rw₂ : (γ₁.comp γ₂).φQ = γ₁.φQ ≫ γ₂.φQ
Tactic: rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
    RightHomologyMapData.comp_φQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ opcyclesMap' φ₂ h₂ h₃
rw₁ : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ γ₂.φQ
rw₂ : (γ₁.comp γ₂).φQ = γ₁.φQ ≫ γ₂.φQ
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
have rw₃ : γ₁.φQ ≫ γ₂.φQ = γ₁.φQ ≫ γ₂.φQ
Tactic: rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
    RightHomologyMapData.comp_φQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw : rightHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
Tactic: rw [← rightHomologyMap'_comp, e.hom_inv_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
⊢ rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw₁ : rightHomologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.H
Tactic: rw [← rightHomologyMap'_comp, e.hom_inv_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
rw₁ : rightHomologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.H
⊢ rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw₂ : Eq.{v_1 + 1} (α := h₁.H ⟶ h₁.H) (𝟙 h₁.H) (𝟙 h₁.H)
Tactic: rw [← rightHomologyMap'_comp, e.hom_inv_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw : rightHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
Tactic: rw [← rightHomologyMap'_comp, e.inv_hom_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
⊢ rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw₁ : rightHomologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.H
Tactic: rw [← rightHomologyMap'_comp, e.inv_hom_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
rw₁ : rightHomologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.H
⊢ rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw₂ : Eq.{v_1 + 1} (α := h₂.H ⟶ h₂.H) (𝟙 h₂.H) (𝟙 h₂.H)
Tactic: rw [← rightHomologyMap'_comp, e.inv_hom_id, rightHomologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' e.hom h₁ h₂ ≫ opcyclesMap' e.inv h₂ h₁ = 𝟙 h₁.Q
have rw : opcyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.Q
Tactic: rw [← opcyclesMap'_comp, e.hom_inv_id, opcyclesMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : opcyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.Q
⊢ opcyclesMap' e.hom h₁ h₂ ≫ opcyclesMap' e.inv h₂ h₁ = 𝟙 h₁.Q
have rw₁ : opcyclesMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.Q
Tactic: rw [← opcyclesMap'_comp, e.hom_inv_id, opcyclesMap'_id]