-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
lemma biproduct.whiskerEquiv_hom_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).hom =
      biproduct.lift fun k => biproduct.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp)

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
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g (e j) =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g (e j)

Tactic:
simp

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
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ ι g (e j) ≫ π g k = ι f j ≫ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

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
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = 0 ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

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
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

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
j : J
h : ¬k = e j
⊢ e j ≠ k

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
k : K
j : J
h : ¬k = e j
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

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
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ ι g (e j) ≫ π g k = ι f j ≫ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

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:
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).hom = lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

Tactic:
simp only [whiskerEquiv_hom]

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 j => (w j).inv ≫ ι g (e j)) = lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

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
k : K
j : J
h : k = e j
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

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
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g (e j) =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g (e 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
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

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.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
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
exact Ne.symm h

Result:
no goals

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 j => (w j).inv ≫ ι g (e j)) = lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

Tactic:
ext k j

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
k : K
j : J
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

Proof state:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
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
⊢ g (e (e.symm k)) = g k

Tactic:
simp

Result:
no goals

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
k : K
j : J
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

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
k : K
j : J
h : k = e j
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

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
k : K
j : J
h : ¬k = e j
⊢ ι f j ≫ (desc fun j => (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

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
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ 0 = 0 ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals