Simproc for canceling morphisms with their inverses

This module implements the cancelIso simproc, which simplifies the composition of a morphism and its inverse, given an expression of the form f ≫ g.

Assuming f is not a composition (as Category.assoc is tagged @[simp]), if g is not a composition itself, it checks whether f is inverse to g by checking if f has an IsIso instance and then by running push inv on inv f and on g. If the check succeeds, then f ≫ g is rewritten to 𝟙 _.

If g is of the form h ≫ k, the procedure instead checks if f and h are inverses to each other, and the procedure rewrites f ≫ h ≫ k to k if that is the case. This special case is useful as f ≫ (h ≫ k) is in simp-normal form and does not contain f ≫ g directly as a subterm.

For instance, the simproc will successfully rewrite expressions such as F.map (G.map (inv (H.map (e.hom)))) ≫ F.map (G.map (H.map (e.inv))) to 𝟙 _ because CategoryTheory.Functor.map_inv is a @[push ←] lemma, and CategoryTheory.IsIso.Iso.inv_hom is a @[push] lemma.

This procedure is mostly intended as a post-procedure: it will work better if f and g have already been traversed beforehand.

theorem Mathlib.Tactic.CategoryTheory.CancelIso.hom_inv_id_of_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {x y : C} (f : x ⟶ y) [CategoryTheory.IsIso f] (g : y ⟶ x) (h : CategoryTheory.inv f = g) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id x

Version of IsIso.hom_inv_id for internal use of the cancelIso simproc. Do not use.

theorem Mathlib.Tactic.CategoryTheory.CancelIso.hom_inv_id_of_eq_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {x y : C} (f : x ⟶ y) [CategoryTheory.IsIso f] (g : y ⟶ x) (h : CategoryTheory.inv f = g) {z : C} (k : x ⟶ z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k) = k

Version of IsIso.hom_inv_id_assoc for internal use of the cancelIso simproc. Do not use.

def Mathlib.Tactic.CategoryTheory.CancelIso.tryCancelPair (C x y z f g : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Given expressions C x y z f g assumed to represent composable morphisms f : x ⟶ y and g : y ⟶ z in a category C, check if g is equal to the inverse of f by

1. first checking the objects match (i.e x = z).
2. Checking that f is an isomorphism by looking for an IsIso instance, allowing us to write inv f.
3. running push inv on both inv f and g, and checking that the results are equal.

If they are inverse, return a proof of inv f = g. If any of the tests above fail, return none.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.CategoryTheory.CancelIso.cancelIsoSimproc : Lean.Meta.Simp.Simproc

cancelIso simplifies the composition of a morphism and its inverse, given an expression of the form f ≫ g.

Assuming f is not a composition (as Category.assoc is tagged @[simp]), if g is not a composition itself, it checks whether f is inverse to g by checking if f has an IsIso instance and then by running push inv on inv f and on g. If the check succeeds, then f ≫ g is rewritten to 𝟙 _.

If g is of the form h ≫ k, the procedure instead checks if f and h are inverses to each other, and the procedure rewrites f ≫ h ≫ k to k if that is the case. This special case is useful as f ≫ (h ≫ k) is in simp-normal form and does not contain f ≫ g directly as a subterm.

For instance, the simproc will successfully rewrite expressions such as F.map (G.map (inv (H.map (e.hom)))) ≫ F.map (G.map (H.map (e.inv))) to 𝟙 _ because CategoryTheory.Functor.map_inv is a @[push ←] lemma, and CategoryTheory.IsIso.Iso.inv_hom is a @[push] lemma.

This procedure is mostly intended as a post-procedure: it will work better if f and g have already been traversed beforehand.

Equations

• One or more equations did not get rendered due to their size.

def cancelIso : Lean.Meta.Simp.Simproc

cancelIso simplifies the composition of a morphism and its inverse, given an expression of the form f ≫ g.

Assuming f is not a composition (as Category.assoc is tagged @[simp]), if g is not a composition itself, it checks whether f is inverse to g by checking if f has an IsIso instance and then by running push inv on inv f and on g. If the check succeeds, then f ≫ g is rewritten to 𝟙 _.

If g is of the form h ≫ k, the procedure instead checks if f and h are inverses to each other, and the procedure rewrites f ≫ h ≫ k to k if that is the case. This special case is useful as f ≫ (h ≫ k) is in simp-normal form and does not contain f ≫ g directly as a subterm.

For instance, the simproc will successfully rewrite expressions such as F.map (G.map (inv (H.map (e.hom)))) ≫ F.map (G.map (H.map (e.inv))) to 𝟙 _ because CategoryTheory.Functor.map_inv is a @[push ←] lemma, and CategoryTheory.IsIso.Iso.inv_hom is a @[push] lemma.

This procedure is mostly intended as a post-procedure: it will work better if f and g have already been traversed beforehand.

Equations

• cancelIso = Mathlib.Tactic.CategoryTheory.CancelIso.cancelIsoSimproc