[Merged by Bors] - feat: quasi-isomorphisms of short complexes

[joelriou]

---

[jcommelin]

You are essentially duplicating every instance as a lemma. But since Lean 4 permits named variables, I wonder whether it is enough to just provide the instances and give nice names to the instance variables:

Suggested change

	lemma quasiIso_comp' (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) (hφ : QuasiIso φ) (hφ' : QuasiIso φ') :
	QuasiIso (φ ≫ φ') := by
	rw [quasiIso_iff] at hφ hφ' ⊢
	rw [homologyMap_comp]
	infer_instance
	instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [QuasiIso φ] [QuasiIso φ'] :
	QuasiIso (φ ≫ φ') :=
	quasiIso_comp' φ φ' inferInstance inferInstance
	instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] :
	QuasiIso (φ ≫ φ') := by
	rw [quasiIso_iff] at hφ hφ' ⊢
	rw [homologyMap_comp]
	infer_instance

This can then be used as quasiIso_comp φ φ' (hφ := foo) (hφ' := bar) when needed.

[joelriou]

Thanks! I have struggled a little bit with the syntax to make this work downstream, but it works. (It seems the exact syntax would be quasiIso_comp (hφ := foo) (hφ' := bar) because from the type of hφ, Lean would find the type of φ!)

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style