awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
    (Quiver.Hom.op (Hom.f (truncLE'Map φ e) i))
    (Quiver.Hom.op (Iso.hom (K.truncLE'XIso e h hi) ≫ φ.f i' ≫ Iso.inv (L.truncLE'XIso e h hi)))

Tactic:
simpa using truncGE'Map_f_eq ((opFunctor C c').map φ.op) e.op (by simpa) h

Premises used: Quiver.Hom.op, CategoryTheory.Functor.map, HomologicalComplex.opFunctor, ComplexShape.Embedding.op, HomologicalComplex.truncGE'Map_f_eq
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
⊢ truncLE'Map (𝟙 K) e = 𝟙 (K.truncLE' e)

Tactic:
(unopFunctor C c.symm).congr_map (congr_arg Quiver.Hom.op (K.op.truncGE'Map_id e.op))

Premises used: HomologicalComplex.unop, HomologicalComplex.op, HomologicalComplex.id, Quiver.Hom.op, HomologicalComplex.truncLE', Quiver.Hom.unop, HomologicalComplex.truncLE'Map, congr_arg, ComplexShape.Embedding.op, HomologicalComplex.truncGE', HomologicalComplex.truncGE'Map_id, CategoryTheory.Functor.congr_map, ComplexShape.symm, HomologicalComplex.unopFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
⊢ Eq (α := K.truncLE' e ⟶ M.truncLE' e) (truncLE'Map (φ ≫ φ') e)
    (CategoryStruct.comp (Y := L.truncLE' e) (truncLE'Map φ e) (truncLE'Map φ' e))

Tactic:
(unopFunctor C c.symm).congr_map (congr_arg Quiver.Hom.op
    (truncGE'Map_comp ((opFunctor C c').map φ'.op) ((opFunctor C c').map φ.op) e.op))

Premises used: HomologicalComplex.unop, HomologicalComplex.op, Quiver.Hom.op, HomologicalComplex.truncLE', HomologicalComplex.truncGE'Map_comp, Quiver.Hom.unop, HomologicalComplex.truncLE'Map, CategoryTheory.Functor.map, congr_arg, HomologicalComplex.opFunctor, ComplexShape.Embedding.op, HomologicalComplex.truncGE', HomologicalComplex.comp, CategoryTheory.Functor.congr_map, ComplexShape.symm, HomologicalComplex.unopFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ truncLEMap (𝟙 K) e = 𝟙 (K.truncLE e)

Tactic:
(unopFunctor C c'.symm).congr_map (congr_arg Quiver.Hom.op (K.op.truncGEMap_id e.op))

Premises used: HomologicalComplex.unop, HomologicalComplex.op, HomologicalComplex.id, Quiver.Hom.op, Quiver.Hom.unop, HomologicalComplex.truncGE, HomologicalComplex.extend, congr_arg, HomologicalComplex.truncLE, ComplexShape.Embedding.op, HomologicalComplex.truncLEMap, CategoryTheory.Functor.congr_map, ComplexShape.symm, HomologicalComplex.unopFunctor, HomologicalComplex.truncGEMap_id
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
change :
  IsIso (X := Opposite.unop ((K.op.truncGE' e.op).X i)) (Quiver.Hom.unop (Hom.f (K.op.restrictionToTruncGE' e.op) i))
⊢ IsIso (X := (K.truncLE' e).X i) (Hom.f (K.truncLE'ToRestriction e) i)

Tactic:
change IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Premises used: CategoryTheory.IsIso, HomologicalComplex.Hom.f, HomologicalComplex.op, Quiver.Hom.unop, ComplexShape.Embedding.op, HomologicalComplex.restrictionToTruncGE'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso (X := (K.op.restriction e.op).X i) (Y := (K.op.truncGE' e.op).X i) (Hom.f (K.op.restrictionToTruncGE' e.op) i)

Tactic:
have := K.op.isIso_restrictionToTruncGE' e.op i (by simpa)
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
this :
  IsIso (X := (K.op.restriction e.op).X i) (Y := (K.op.truncGE' e.op).X i) (Hom.f (K.op.restrictionToTruncGE' e.op) i)
⊢ IsIso (X := Opposite.unop ((K.op.truncGE' e.op).X i)) (Quiver.Hom.unop (Hom.f (K.op.restrictionToTruncGE' e.op) i))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
⊢ Eq (α := K.truncLE' e ⟶ L.restriction e)
    (CategoryStruct.comp (Y := L.truncLE' e) (truncLE'Map φ e) (L.truncLE'ToRestriction e))
    (K.truncLE'ToRestriction e ≫ restrictionMap φ e)

Tactic:
(unopFunctor C c.symm).congr_map (congr_arg Quiver.Hom.op
    (restrictionToTruncGE'_naturality ((opFunctor C c').map φ.op) e.op))

Premises used: HomologicalComplex.unop, HomologicalComplex.op, Quiver.Hom.op, HomologicalComplex.truncLE', Quiver.Hom.unop, HomologicalComplex.restriction, CategoryTheory.Functor.map, congr_arg, HomologicalComplex.opFunctor, ComplexShape.Embedding.op, HomologicalComplex.truncGE', HomologicalComplex.comp, HomologicalComplex.restrictionToTruncGE'_naturality, CategoryTheory.Functor.congr_map, ComplexShape.symm, HomologicalComplex.unopFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
i : ι
⊢ Mono (X := (K.truncLE' e).X i) (Hom.f (K.truncLE'ToRestriction e) i)

Tactic:
inferInstanceAs (Mono ((K.op.restrictionToTruncGE' e.op).f i).unop)

Premises used: _private.0.HomologicalComplex.instMonoFTruncLE'ToRestriction._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
⊢ IsIso (X := (K.truncLE' e).X i) (Hom.f (K.truncLE'ToRestriction e) i)

Tactic:
inferInstanceAs (IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop)

Premises used: _private.0.HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
⊢ Mono (X := (K.truncLE e).X i') (Hom.f (K.ιTruncLE e) i')

Tactic:
inferInstanceAs (Mono ((K.op.πTruncGE e.op).f i').unop)

Premises used: _private.0.HomologicalComplex.instMonoFιTruncLE._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
⊢ Mono (X := K.truncLE e) (K.ιTruncLE e)

Tactic:
mono_of_mono_f _ (fun _ => inferInstance)

Premises used: inferInstance, HomologicalComplex.mono_of_mono_f
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
rw : (K.truncLE e).op.IsStrictlySupported e.op
⊢ (K.truncLE e).IsStrictlySupported e

Tactic:
rw [← isStrictlySupported_op_iff]

Premises used: HomologicalComplex.isStrictlySupported_op_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
⊢ (K.truncLE e).op.IsStrictlySupported e.op

Tactic:
inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e.op)

Premises used: _private.0.HomologicalComplex.instIsStrictlySupportedTruncLE._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
⊢ (K.truncLE e).op.IsStrictlySupported e.op

Tactic:
exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e.op)
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
⊢ Eq (α := K.truncLE e ⟶ L) (CategoryStruct.comp (Y := L.truncLE e) (truncLEMap φ e) (L.ιTruncLE e)) (K.ιTruncLE e ≫ φ)

Tactic:
(unopFunctor C c'.symm).congr_map (congr_arg Quiver.Hom.op
    (πTruncGE_naturality ((opFunctor C c').map φ.op) e.op))

Premises used: HomologicalComplex.unop, HomologicalComplex.op, Quiver.Hom.op, Quiver.Hom.unop, HomologicalComplex.truncGE, HomologicalComplex.extend, CategoryTheory.Functor.map, congr_arg, HomologicalComplex.opFunctor, HomologicalComplex.πTruncGE_naturality, HomologicalComplex.truncLE, ComplexShape.Embedding.op, HomologicalComplex.comp, CategoryTheory.Functor.congr_map, ComplexShape.symm, HomologicalComplex.unopFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
rw : (K.truncLE e).op.IsStrictlySupported e'.op
⊢ (K.truncLE e).IsStrictlySupported e'

Tactic:
rw [← isStrictlySupported_op_iff]

Premises used: HomologicalComplex.isStrictlySupported_op_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
⊢ (K.truncLE e).op.IsStrictlySupported e'.op

Tactic:
inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e'.op)

Premises used: _private.0.HomologicalComplex.instIsStrictlySupportedTruncLE_1._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
⊢ (K.truncLE e).op.IsStrictlySupported e'.op

Tactic:
exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e'.op)
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
⊢ IsIso (X := K.truncLE e) (K.ιTruncLE e)

Tactic:
inferInstanceAs (IsIso ((unopFunctor C c'.symm).map (K.op.πTruncGE e.op).op))

Premises used: _private.0.HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ IsIso (X := K.truncLE e) (K.ιTruncLE e) ↔ K.IsStrictlySupported e

Tactic:
⟨fun _ ↦ isStrictlySupported_of_iso (asIso (K.ιTruncLE e)) e,
    fun _ ↦ inferInstance⟩

Premises used: HomologicalComplex.ιTruncLE, inferInstance, Iff.intro, HomologicalComplex.isStrictlySupported_of_iso, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
⊢ (K.op.restriction e.op).HasHomology j

Tactic:
have : (K.op.restriction e.op).HasHomology j :=
    inferInstanceAs ((K.restriction e).op.HasHomology j)
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
rw : QuasiIsoAt (K := K.op.restriction e.op) (L := K.op.truncGE' e.op) (K.op.restrictionToTruncGE' e.op) j
⊢ QuasiIsoAt (K := K.truncLE' e) (L := K.restriction e)
    (CategoryTheory.Functor.map (unopFunctor C c.symm) (Quiver.Hom.op (K.op.restrictionToTruncGE' e.op)) :
      Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.truncGE' e.op)) ⟶
        Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.restriction e.op)))
    j

Tactic:
rw [quasiIsoAt_unopFunctor_map_iff]

Premises used: HomologicalComplex.quasiIsoAt_unopFunctor_map_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
⊢ ¬e.op.BoundaryGE j

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
⊢ QuasiIsoAt (K := K.op.restriction e.op) (L := K.op.truncGE' e.op) (K.op.restrictionToTruncGE' e.op) j

Tactic:
exact truncGE'.quasiIsoAt_restrictionToTruncGE' K.op e.op j (by simpa)

Premises used: HomologicalComplex.op, ComplexShape.Embedding.op, HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
⊢ (K.truncLE' e).HasHomology i

Tactic:
inferInstanceAs ((K.op.truncGE' e.op).unop.HasHomology i)

Premises used: _private.0.HomologicalComplex.truncLE'.truncLE'_hasHomology._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i' : ι'
⊢ (K.truncLE e).HasHomology i'

Tactic:
inferInstanceAs ((K.op.truncGE e.op).unop.HasHomology i')

Premises used: _private.0.HomologicalComplex.instHasHomologyTruncLE._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (L := K.op.truncGE e.op) (K.op.πTruncGE e.op) j'

Tactic:
have := K.op.quasiIsoAt_πTruncGE e.op hj'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
this : QuasiIsoAt (L := K.op.truncGE e.op) (K.op.πTruncGE e.op) j'
⊢ QuasiIsoAt (K := K.truncLE e) (K.ιTruncLE e) j'

Tactic:
inferInstanceAs (QuasiIsoAt ((unopFunctor _ _).map (K.op.πTruncGE e.op).op) j')

Premises used: _private.0.HomologicalComplex.quasiIsoAt_ιTruncLE._proof_1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
this : QuasiIsoAt (L := K.op.truncGE e.op) (K.op.πTruncGE e.op) j'
⊢ QuasiIsoAt (K := K.truncLE e) (K.ιTruncLE e) j'

Tactic:
exact inferInstanceAs (QuasiIsoAt ((unopFunctor _ _).map (K.op.πTruncGE e.op).op) j')
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i : ι
⊢ QuasiIsoAt (K := K.truncLE e) (K.ιTruncLE e) (e.f i)

Tactic:
K.quasiIsoAt_ιTruncLE e rfl

Premises used: HomologicalComplex.quasiIsoAt_ιTruncLE, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
rw :
  QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op K)) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (K.ιTruncLE e))) ↔
    K.op.IsSupported e.op
⊢ QuasiIso (K := K.truncLE e) (K.ιTruncLE e) ↔ K.IsSupported e

Tactic:
rw [← quasiIso_opFunctor_map_iff, ← isSupported_op_iff]

Premises used: HomologicalComplex.isSupported_op_iff, HomologicalComplex.quasiIso_opFunctor_map_iff