-- Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
/-- A 2-square is Guitart exact iff it is so after replacing the left and right functors by
isomorphic functors. -/
@[simp]
lemma whiskerVertical_iff (α : L ≅ L') (β : R ≅ R') :
    (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact

Proof state:
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
X₁ : C₁
⊢ w.natTrans.app X₁ = ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).natTrans.app X₁

Tactic:
simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
  ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]

Result:
no goals

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
⊢ w.GuitartExact → (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
intro h

Result:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : w.GuitartExact
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : w.GuitartExact
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
exact whiskerVertical w α β

Result:
no goals

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact

Tactic:
intro h

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ w.GuitartExact

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact

Tactic:
exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact

Tactic:
constructor

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact

case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
⊢ w.GuitartExact → (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_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom

Tactic:
ext X₁

Result:
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
X₁ : C₁
⊢ w.natTrans.app X₁ = ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).natTrans.app X₁

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ w.GuitartExact

Tactic:
rw [this]

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ w.GuitartExact

Tactic:
have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom := by
  ext X₁
  simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
    ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_7, u_2} C₂
inst✝¹ : Category.{u_10, u_4} D₁
inst✝ : Category.{u_9, 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₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ w.GuitartExact