-- Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
/-- A 2-square stays Guitart exact if we replace the left and right functors
by isomorphic functors. See also `whiskerVertical_iff`. -/
lemma whiskerVertical [w.GuitartExact] (α : L ≅ L') (β : R ≅ R') :
    (w.whiskerVertical α.hom β.inv).GuitartExact

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (R'.map f.hom ≫ β.inv.app (T.obj f.right) ≫ w.natTrans.app f.right ≫ B.map (α.hom.app f.right)) ≫
      B.map (α.inv.app f.right) =
    β.inv.app X₂ ≫ R.map f.hom ≫ w.app f.right

Tactic:
simp only [NatTrans.naturality_assoc, assoc, NatIso.cancel_natIso_inv_left, ← B.map_comp,
  Iso.hom_inv_id_app, B.map_id, comp_id]

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).obj f).hom ≫ B.map (α.symm.app f.right).hom =
    ((w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor).obj f).hom

Tactic:
dsimp

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (R'.map f.hom ≫ β.inv.app (T.obj f.right) ≫ w.natTrans.app f.right ≫ B.map (α.hom.app f.right)) ≫
      B.map (α.inv.app f.right) =
    β.inv.app X₂ ≫ R.map f.hom ≫ w.app f.right

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Tactic:
rw [Functor.initial_natIso_iff e]

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ (w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor).Initial

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ ∀ (X₂ : D₁), ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Tactic:
let e : structuredArrowDownwards (w.whiskerVertical α.hom β.inv) X₂ ≅
    w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂) ).functor :=
  NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) (by
    dsimp
    simp only [NatTrans.naturality_assoc, assoc, NatIso.cancel_natIso_inv_left, ← B.map_comp,
      Iso.hom_inv_id_app, B.map_id, comp_id]))

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ (w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor).Initial

Tactic:
infer_instance

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ ∀ (X₂ : D₁), ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Tactic:
intro X₂

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_9, u_2} C₂
inst✝² : Category.{u_8, u_4} D₁
inst✝¹ : Category.{u_10, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial