awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
⊢ Eq (α :=
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
        (ε (F.mapAction G))))
    (Hom.hom (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))
have h : CategoryStruct.comp (Y := tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (ε F) =
  𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
⊢ CategoryStruct.comp (Y := tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
have h : Eq.{v_2 + 1} (α := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
  (𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))) (𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
Tactic: rw [η_ε]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
      (δ (F.mapAction G) x x_1) =
    𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
have h : Hom.hom
    (CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
      (δ (F.mapAction G) x x_1)) =
  Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
        (δ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1)))
have h : CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)) (μ F x.V x_1.V) (δ F x.V x_1.V) =
  𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)) (μ F x.V x_1.V) (δ F x.V x_1.V) =
    𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))
have h : Eq.{v_2 + 1} (α :=
  tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V) ⟶
    tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))
  (𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)))
  (𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)))
Tactic: rw [μ_δ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
      (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1) =
    𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))
have h : Hom.hom
    (CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
      (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1)) =
  Hom.hom (𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
        (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)))
have h : CategoryStruct.comp (Y := tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)) (δ F x.V x_1.V)
    (μ F x.V x_1.V) =
  𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
⊢ CategoryStruct.comp (Y := tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)) (δ F x.V x_1.V)
      (μ F x.V x_1.V) =
    𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))
have h : Eq.{v_2 + 1} (α :=
  F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))
  (𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))) (𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)))
Tactic: rw [δ_μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : SingleObj M
⊢ (↾fun (x_1 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_1) = 𝟙 X
have h : ∀ (x_1 : X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_2 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_2)) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
X_1 Y Z : SingleObj M
f : X_1 ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α := X ⟶ X) (↾fun (x : X) ↦ f ≫ g • x)
    (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x))
have h : ∀ (x : X),
  Eq (α := X) (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : X) ↦ f ≫ g • x)) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x)))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : ActionCategory M X
⊢ Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) () x.back = x
have mk : ∀ (fst : SingleObj M) (snd : Functor.obj (actionAsFunctor M X) fst),
  Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) ()
      (ActionCategory.back (Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd)) =
    Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P f
have refine : P (homOfPair b.back (↑f : a.fst ⟶ b.fst)) = P f
Tactic: refine cast ?_ (hyp b.back f.val)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P (homOfPair b.back (↑f : a.fst ⟶ b.fst)) = P f
have rcases : ∀ (a : X) (f : Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a ⟶ b),
  P (homOfPair b.back (↑f : ⟨PUnit.unit, a⟩.fst ⟶ b.fst)) = P f
Tactic: rcases a with ⟨⟨⟩, a : X⟩
Cleared hypotheses: a, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
b : ActionCategory G X
a : X
f : Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a ⟶ b
⊢ P (homOfPair b.back (↑f : ⟨PUnit.unit, a⟩.fst ⟶ b.fst)) = P f
have rcases : ∀ (b : X)
  (f :
    Quiver.Hom.{u_2, u} (V := ActionCategory G X)
      (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a)
      (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)),
  P (a :=
      Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) ()
        (HSMul.hSMul (β := X) (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)⁻¹
          (ActionCategory.back.{u, u_2} (M := G)
            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
      (homOfPair
        (ActionCategory.back.{u, u_2} (M := G)
          (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))
        (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)) =
    P f
Tactic: rcases b with ⟨⟨⟩, b : X⟩
Cleared hypotheses: b, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
    IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
have h₁ : IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
  IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'
Tactic: use (pullback αX f), (pullback.fst αX f), l, (pullback.snd αX f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
    IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'
have h₁ : IsPullback l (pullback.snd αX f) αY g
Tactic: refine ⟨IsPullback.of_hasPullback αX f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ : IsPullback l (pullback.snd αX f) αY g
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
    IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'
have h₂ : IsPushout (pullback.fst αX f) l h' i'
Tactic: refine ⟨IsPullback.of_hasPullback αX f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback l (pullback.snd αX f) αY g
have h₁ : IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)
Tactic: refine IsPullback.of_right' ?_ hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)
have h₁ : IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)
Tactic: rw [← H.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPushout (pullback.fst αX f) l h' i'
have h₁ : IsPullback l (pullback.snd αX f) αY g
Tactic: refine (H' (pullback.fst αX f) l h' i' (pullback.snd αX f) αX αY αZ
      (IsPullback.of_hasPullback αX f) ?_
        hh.toCommSq hi.toCommSq ⟨by simp only [IsPullback.lift_fst, l]⟩).2 ⟨hh, hi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
⊢ H.IsVanKampen ↔ IsVanKampenColimit (PushoutCocone.mk h i ⋯)
have mp : H.IsVanKampen → IsVanKampenColimit (PushoutCocone.mk h i sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H : IsPushout f g h i
mp : H.IsVanKampen → IsVanKampenColimit (PushoutCocone.mk h i ⋯)
⊢ H.IsVanKampen ↔ IsVanKampenColimit (PushoutCocone.mk h i ⋯)
have mpr : IsVanKampenColimit (PushoutCocone.mk h i sorry) → H.IsVanKampen
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
have mp : Nonempty (IsColimit c') ↔
  IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
Tactic: refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
have mp₁ : CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
Tactic: refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
mp₁ : CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
have mp₂ : CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
Tactic: refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
mp₁ : CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
mp₂ : CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
have mp₃ : CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
  (c'.ι.app WalkingSpan.right)
Tactic: refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
mp₁ : CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
mp₂ : CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
mp₃ :
  CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
have mp₄ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
  ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i sorry).ι.app j)
Tactic: refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
have this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
Tactic: have : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left =
          F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right := by
        simp only [Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
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
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
have mp : Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
  IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
Tactic: rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this)
            _).nonempty_congr]