-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem normalizeObj_congr (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶ Y) :
    normalizeObj X n = normalizeObj Y n

Proof state:
case mk.h.whiskerLeft.h
C : Type u
X Y X✝ Y₁✝ Y₂✝ : F C
f✝ : Y₁✝ ⟶ᵐ Y₂✝
ih : (fun n => Y₁✝.normalizeObj n) = Y₂✝.normalizeObj
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor Y₁✝).normalizeObj x✝ = (X✝.tensor Y₂✝).normalizeObj x✝

Tactic:
apply congr_fun ih

Result:
no goals

Proof state:
case mk
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
⊢ X.normalizeObj n = Y.normalizeObj n

Tactic:
apply @congr_fun _ _ fun n => normalizeObj X n

Result:
case mk.h
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
⊢ (fun n => X.normalizeObj n) = Y.normalizeObj

Proof state:
case mk.h.tensor.h
C : Type u
X✝ Y✝ W X Y Z : F C
f✝ : W ⟶ᵐ Y
g✝ : X ⟶ᵐ Z
ih₁ : (fun n => W.normalizeObj n) = Y.normalizeObj
ih₂ : (fun n => X.normalizeObj n) = Z.normalizeObj
n : NormalMonoidalObject C
⊢ (W.tensor X).normalizeObj n = (Y.tensor Z).normalizeObj n

Tactic:
simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]

Result:
no goals

Proof state:
case mk.h
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
⊢ (fun n => X.normalizeObj n) = Y.normalizeObj

Tactic:
clear n f

Result:
case mk.h
C : Type u
X Y : F C
f' : X ⟶ᵐ Y
⊢ (fun n => X.normalizeObj n) = Y.normalizeObj

Proof state:
case mk.h
C : Type u
X Y : F C
f' : X ⟶ᵐ Y
⊢ (fun n => X.normalizeObj n) = Y.normalizeObj

Tactic:
induction f' with
| comp _ _ _ _ => apply Eq.trans <;> assumption
| whiskerLeft  _ _ ih => funext; apply congr_fun ih
| whiskerRight _ _ ih => funext; apply congr_arg₂ _ rfl (congr_fun ih _)
| @tensor W X Y Z _ _ ih₁ ih₂ =>
    funext n
    simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]
| _ => funext; rfl

Result:
no goals

Proof state:
case mk.h.whiskerRight
C : Type u
X Y X₁✝ X₂✝ : F C
f✝ : X₁✝ ⟶ᵐ X₂✝
Y✝ : F C
ih : (fun n => X₁✝.normalizeObj n) = X₂✝.normalizeObj
⊢ (fun n => (X₁✝.tensor Y✝).normalizeObj n) = (X₂✝.tensor Y✝).normalizeObj

Tactic:
funext

Result:
case mk.h.whiskerRight.h
C : Type u
X Y X₁✝ X₂✝ : F C
f✝ : X₁✝ ⟶ᵐ X₂✝
Y✝ : F C
ih : (fun n => X₁✝.normalizeObj n) = X₂✝.normalizeObj
x✝ : NormalMonoidalObject C
⊢ (X₁✝.tensor Y✝).normalizeObj x✝ = (X₂✝.tensor Y✝).normalizeObj x✝

Proof state:
case mk.h.comp
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n => X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n => Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ (fun n => X✝.normalizeObj n) = Z✝.normalizeObj

Tactic:
apply Eq.trans <;> assumption

Result:
no goals

Proof state:
case mk.h.whiskerRight.h
C : Type u
X Y X₁✝ X₂✝ : F C
f✝ : X₁✝ ⟶ᵐ X₂✝
Y✝ : F C
ih : (fun n => X₁✝.normalizeObj n) = X₂✝.normalizeObj
x✝ : NormalMonoidalObject C
⊢ (X₁✝.tensor Y✝).normalizeObj x✝ = (X₂✝.tensor Y✝).normalizeObj x✝

Tactic:
apply congr_arg₂ _ rfl (congr_fun ih _)

Result:
no goals

Proof state:
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
⊢ X.normalizeObj n = Y.normalizeObj n

Tactic:
rcases f with ⟨f'⟩

Result:
case mk
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
⊢ X.normalizeObj n = Y.normalizeObj n

Proof state:
case mk.h.whiskerLeft
C : Type u
X Y X✝ Y₁✝ Y₂✝ : F C
f✝ : Y₁✝ ⟶ᵐ Y₂✝
ih : (fun n => Y₁✝.normalizeObj n) = Y₂✝.normalizeObj
⊢ (fun n => (X✝.tensor Y₁✝).normalizeObj n) = (X✝.tensor Y₂✝).normalizeObj

Tactic:
funext

Result:
case mk.h.whiskerLeft.h
C : Type u
X Y X✝ Y₁✝ Y₂✝ : F C
f✝ : Y₁✝ ⟶ᵐ Y₂✝
ih : (fun n => Y₁✝.normalizeObj n) = Y₂✝.normalizeObj
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor Y₁✝).normalizeObj x✝ = (X✝.tensor Y₂✝).normalizeObj x✝

Proof state:
case mk.h.tensor
C : Type u
X✝ Y✝ W X Y Z : F C
f✝ : W ⟶ᵐ Y
g✝ : X ⟶ᵐ Z
ih₁ : (fun n => W.normalizeObj n) = Y.normalizeObj
ih₂ : (fun n => X.normalizeObj n) = Z.normalizeObj
⊢ (fun n => (W.tensor X).normalizeObj n) = (Y.tensor Z).normalizeObj

Tactic:
funext n

Result:
case mk.h.tensor.h
C : Type u
X✝ Y✝ W X Y Z : F C
f✝ : W ⟶ᵐ Y
g✝ : X ⟶ᵐ Z
ih₁ : (fun n => W.normalizeObj n) = Y.normalizeObj
ih₂ : (fun n => X.normalizeObj n) = Z.normalizeObj
n : NormalMonoidalObject C
⊢ (W.tensor X).normalizeObj n = (Y.tensor Z).normalizeObj n

Proof state:
case mk.h.ρ_inv.h
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (X✝.tensor unit).normalizeObj x✝

Tactic:
rfl

Result:
no goals

Proof state:
case mk.h.ρ_inv
C : Type u
X Y X✝ : F C
⊢ (fun n => X✝.normalizeObj n) = (X✝.tensor unit).normalizeObj

Tactic:
funext

Result:
case mk.h.ρ_inv.h
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (X✝.tensor unit).normalizeObj x✝