-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
lemma biproduct.whiskerEquiv_inv_eq_lift {f : J → C} {g : K → C} (e : J ≃ K)
    (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
    (biproduct.whiskerEquiv e w).inv =
      biproduct.lift fun j => biproduct.π g (e j) ≫ (w j).hom

Proof state:
case w.w
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
by_cases h : k = e j

Result:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : k = e j
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Proof state:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
h : ¬k = e (e.symm k)
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

Tactic:
exact h

Result:
no goals

Proof state:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k) ≫ π f j = ι g k ≫ π g (e j) ≫ (w j).hom

Tactic:
rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]

Result:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = 0 ≫ (w j).hom

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Proof state:
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (whiskerEquiv e w).inv = lift fun j => π g (e j) ≫ (w j).hom

Tactic:
simp only [whiskerEquiv_inv]

Result:
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) = lift fun j => π g (e j) ≫ (w j).hom

Proof state:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
⊢ ι g (e j) ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g (e j) ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
  Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
  lift_π, bicone_ι_π_self_assoc]

Result:
no goals

Proof state:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
simp only [ι_desc_assoc, Category.assoc, ne_eq, lift_π]

Result:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k) ≫ π f j = ι g k ≫ π g (e j) ≫ (w j).hom

Proof state:
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) = lift fun j => π g (e j) ≫ (w j).hom

Tactic:
ext j k

Result:
case w.w
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Proof state:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : k = e j
⊢ ι g k ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
subst h

Result:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
⊢ ι g (e j) ≫ (desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g (e j) ≫ (lift fun j => π g (e j) ≫ (w j).hom) ≫ π f j

Proof state:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
rintro rfl

Result:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
h : ¬k = e (e.symm k)
⊢ False

Proof state:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ 0 = 0 ≫ (w j).hom

Tactic:
simp

Result:
no goals