-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
@[simp]
lemma i_cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂)
    (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) :
    (forget₂ C Ab).map S.iCycles (S.cyclesMk x₂ hx₂) = x₂

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Tactic:
rw [← ConcreteCategory.comp_apply, S.mapCyclesIso_hom_iCycles (forget₂ C Ab), this]

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Tactic:
have := abCyclesIso_inv_apply_iCycles (S.map (forget₂ C Ab)) ⟨x₂, hx₂⟩

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    ↑⟨x₂, hx₂⟩
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles)) (S.cyclesMk x₂ hx₂) = x₂

Tactic:
dsimp [cyclesMk]

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    ↑⟨x₂, hx₂⟩
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Tactic:
simp only [map_X₂, map_X₃, map_g] at this

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂