awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Nonempty.{v₂ + 1} (Arrow.LiftStruct β)
have mp : ∀ (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃),
  Nonempty.{v₂ + 1}
    (Arrow.LiftStruct.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
      ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α))
Tactic: obtain ⟨α, rfl⟩ := (adj₂.arrowHomEquiv sq₁₂ sq₁₃).surjective β
Cleared hypotheses: β
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom
have rw : HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom
Tactic: rw [← hasLiftingProperty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty f (Opposite.op (Arrow.mk g) ⋔ Arrow.mk h).hom
have rw : HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty (Arrow.mk g □ Arrow.mk f).hom h
Tactic: rw [← hasLiftingProperty_mk_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom h ↔ HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
have dsimp : HasLiftingProperty (A := pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (i.to B) g))
    (ι (ofHasPushout (curriedTensor C) (i.to B) g)) h ↔
  HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
⊢ HasLiftingProperty (A := pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (i.to B) g))
      (ι (ofHasPushout (curriedTensor C) (i.to B) g)) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
have this : HasLiftingProperty (A :=
    pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
    (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
  HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h
Tactic: have := HasLiftingProperty.iff_of_arrow_iso_left (isInitialIso' g i (W := B)) h
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
this :
  HasLiftingProperty (A :=
      pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
    HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (A := pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (i.to B) g))
      (ι (ofHasPushout (curriedTensor C) (i.to B) g)) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
have rw : HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B K) (B ◁ g) h ↔
  HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
Tactic: rw [dsimp% this]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
h : X ⟶ Y
i : IsInitial.{v, u} K
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (X := L ⟹ X) f (map (ihom L) h)
have rw : HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (Arrow.mk (i.to L) □ Arrow.mk f).hom h
Tactic: rw [← hasLiftingProperty_mk_isInitial_iff i]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔
    HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)
have rw : HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
  HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)
Tactic: rw [hasLiftingProperty_mk_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
i : IsInitial.{v, u} A
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom (t.from X) ↔
    HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))
have rw : HasLiftingProperty (X := B ⟹ X) g (map (ihom B) (t.from X)) ↔ HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))
Tactic: rw [hasLiftingProperty_mk_isInitial_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
i : IsInitial.{v, u} K
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔
    HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))
have rw : HasLiftingProperty (X := L ⟹ X) f (map (ihom L) (t.from X)) ↔ HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))
Tactic: rw [hasLiftingProperty_mk_isInitial_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Fintype J
j : Bicone J
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) j
have left : Membership.mem (γ := Finset (Bicone J))
  (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.left
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Fintype J
j : Bicone J
left :
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.left
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) j
have right : Membership.mem (γ := Finset (Bicone J))
  (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.right
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Fintype J
j : Bicone J
left :
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.left
right :
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.right
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) j
have diagram : ∀ (val : J),
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) (Bicone.diagram val)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
⊢ Decidable (f = g)
have left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (left_id = g)
Tactic: cases f
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
⊢ Decidable (f = g)
have right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (right_id = g)
Tactic: cases f
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
⊢ Decidable (f = g)
have left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (left j = g)
Tactic: cases f
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
⊢ Decidable (f = g)
have right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (right j = g)
Tactic: cases f
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
⊢ Decidable (f = g)
have diagram : {j k : J} → (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (diagram f = g)
Tactic: cases f
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left
⊢ Decidable (left_id = g)
have left_id : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) left_id left_id)
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right
⊢ Decidable (right_id = g)
have right_id : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) right_id right_id)
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)
⊢ Decidable (left j = g)
have left : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (left j) (left j))
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)
⊢ Decidable (right j = g)
have right : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (right j) (right j))
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)
⊢ Decidable (diagram f = g)
have diagram : (f_1 : j ⟶ k) → Decidable (diagram f = diagram f_1)
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) left_id left_id)
have left_id : Decidable True
Tactic: simp only [diagram.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) right_id right_id)
have right_id : Decidable True
Tactic: simp only [diagram.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (left j) (left j))
have left : Decidable True
Tactic: simp only [diagram.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (right j) (right j))
have right : Decidable True
Tactic: simp only [diagram.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f f_1 : j ⟶ k
⊢ Decidable (diagram f = diagram f_1)
have diagram : Decidable (f = f_1)
Tactic: simp only [diagram.injEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
⊢ Decidable (f = g)
have left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (left_id = g)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
⊢ Decidable (f = g)
have right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (right_id = g)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
⊢ Decidable (f = g)
have left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (left j = g)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
⊢ Decidable (f = g)
have right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (right j = g)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
⊢ Decidable (f = g)
have diagram : {j k : J} → (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (diagram f = g)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₁ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₂ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₃ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
⊢ Decidable (f = g)
have left_id₄ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₁ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₂ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₃ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₄ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
⊢ Decidable (f = g)
have right_id₄ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g