awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Eq (α := pullback m₂ l₁ ⟶ Z) ((snd m₂ l₁ ≫ f₁) ≫ a) ((fst m₂ l₁ ≫ g₂) ≫ b)
i'_w :
  Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) (snd m₂ l₁ ≫ l₁ ≫ f)
    (fst m₂ l₁ ≫ fst g v ≫ g)
i'_w₁ :
  Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) (snd m₂ l₁ ≫ snd f u ≫ u)
    (fst m₂ l₁ ≫ fst g v ≫ g)
i'_w₂ :
  Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) ((snd m₂ l₁ ≫ snd f u) ≫ u)
    (fst m₂ l₁ ≫ fst g v ≫ g)
i'_w₃ :
  CategoryStruct.comp (Y := pullback a b) (pullback.lift (snd m₂ l₁ ≫ f₁) (fst m₂ l₁ ≫ g₂) this) (fst a b ≫ u) =
    fst m₂ l₁ ≫ fst g v ≫ g
i'_w₄ :
  CategoryStruct.comp (Y := pullback a b) (pullback.lift (snd m₂ l₁ ≫ f₁) (fst m₂ l₁ ≫ g₂) this)
      (snd a b ≫ inr (fst a b) (snd a b)) =
    fst m₂ l₁ ≫ fst g v ≫ g
i'_w₅ :
  Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b))
    ((fst m₂ l₁ ≫ g₂) ≫ inr (fst a b) (snd a b)) (fst m₂ l₁ ≫ fst g v ≫ g)
i'_w₆ :
  Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b))
    ((fst m₂ l₁ ≫ g₂) ≫ inr (fst a b) (snd a b)) (fst m₂ l₁ ≫ snd g v ≫ v)
⊢ Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) (fst m₂ l₁ ≫ fst g v ≫ f)
    (fst m₂ l₁ ≫ fst g v ≫ g)
have i'_w₇ : Eq (α := pullback m₂ l₁ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) (fst m₂ l₁ ≫ g₂ ≫ inr (fst a b) (snd a b))
  (fst m₂ l₁ ≫ snd g v ≫ v)
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
⊢ Eq (α := pullback m₂ l₂ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) (fst m₂ l₂ ≫ fst g v ≫ f)
    (fst m₂ l₂ ≫ fst g v ≫ g)
have i'_w : Eq (α := pullback m₂ l₂ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) ((snd m₂ l₂ ≫ snd f v) ≫ v)
  ((fst m₂ l₂ ≫ snd g v) ≫ v)
Tactic: rw [sq₂₂.w_assoc, sq_f_v.w, sq_g_v.w, ← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
⊢ Eq (α := pullback m₂ l₂ ⟶ pushout (X := pullback a b) (fst a b) (snd a b)) ((snd m₂ l₂ ≫ snd f v) ≫ v)
    ((fst m₂ l₂ ≫ snd g v) ≫ v)
have i'_w : Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
Tactic: refine ?_ =≫ v
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w : Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b sorry)
  ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₁ : Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b sorry)
  ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₂ : Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b sorry)
  ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₂ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₃ : Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ g ≫ pushout.desc a b sorry)
  ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₂ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₃ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₄ : Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b sorry) ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₂ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₃ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₄ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₅ : Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b sorry) (fst m₂ l₂ ≫ snd g v ≫ v ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₂ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₃ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₄ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₅ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯) (fst m₂ l₂ ≫ snd g v ≫ v ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)
have i'_w₆ : Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b sorry) (fst m₂ l₂ ≫ fst g v ≫ g ≫ pushout.desc a b sorry)
Tactic: rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
⊢ Adhesive (Functor.{v'', v, u'', u} D C)
have van_kampen : ∀ {W X Y Z : Functor.{v'', v, u'', u} D C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f]
  (H : IsPushout f g h i), H.IsVanKampen
Tactic: constructor