Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case i'_w.h'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := ⋯
v : B ⟶ pushout (fst a b) (snd a b) := ⋯
this✝¹ : Mono u := ⋯
this✝ : Mono v := ⋯
sq_f_u : IsPullback (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := ⋯
f₁ : pullback f u ⟶ A := ⋯
l₂ : pullback f v ⟶ K := ⋯
f₂ : pullback f v ⟶ B := ⋯
m₁ : pullback g u ⟶ K := ⋯
g₁ : pullback g u ⟶ A := ⋯
m₂ : pullback g v ⟶ K := ⋯
g₂ : pullback g v ⟶ B := ⋯
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
⊢ fst m₂ l₁ ≫ fst g v ≫ f = fst m₂ l₁ ≫ fst g v ≫ g

pp: case i'_w.i'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := ⋯
v : B ⟶ pushout (fst a b) (snd a b) := ⋯
this✝¹ : Mono u := ⋯
this✝ : Mono v := ⋯
sq_f_u : IsPullback (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := ⋯
f₁ : pullback f u ⟶ A := ⋯
l₂ : pullback f v ⟶ K := ⋯
f₂ : pullback f v ⟶ B := ⋯
m₁ : pullback g u ⟶ K := ⋯
g₁ : pullback g u ⟶ A := ⋯
m₂ : pullback g v ⟶ K := ⋯
g₂ : pullback g v ⟶ B := ⋯
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
⊢ fst m₂ l₂ ≫ fst g v ≫ f = fst m₂ l₂ ≫ fst g v ≫ g

Tactic:
· have : (pullback.snd m₂ l₁ ≫ f₁) ≫ a = (pullback.fst m₂ l₁ ≫ g₂) ≫ b := by
          rw [← _ ≫= pushout.inl_desc a b pullback.condition, Category.assoc, ← sq_f_u.w_assoc,
            w, ← sq₂₁.w_assoc, Category.assoc, sq_g_v.w_assoc, pushout.inr_desc]
        rw [sq₂₁.w_assoc, sq_f_u.w, ← Category.assoc, ← pullback.lift_fst_assoc _ _ this,
          pushout.condition, pullback.lift_snd_assoc _ _ this, sq_g_v.w, Category.assoc]

Goal state after:
case i'_w.i'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := ⋯
v : B ⟶ pushout (fst a b) (snd a b) := ⋯
this✝¹ : Mono u := ⋯
this✝ : Mono v := ⋯
sq_f_u : IsPullback (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := ⋯
f₁ : pullback f u ⟶ A := ⋯
l₂ : pullback f v ⟶ K := ⋯
f₂ : pullback f v ⟶ B := ⋯
m₁ : pullback g u ⟶ K := ⋯
g₁ : pullback g u ⟶ A := ⋯
m₂ : pullback g v ⟶ K := ⋯
g₂ : pullback g v ⟶ B := ⋯
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
⊢ fst m₂ l₂ ≫ fst g v ≫ f = fst m₂ l₂ ≫ fst g v ≫ g