awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)
id₁ : ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)
id₂ :
  ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)
have id₃ : ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
  (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)
id₁ : ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)
id₂ :
  ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)
id₃ :
  ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)
have id₄ : ((Hom.id zero).comp Hom.reflexion).comp (Hom.id one) = (Hom.id zero).comp (Hom.reflexion.comp (Hom.id one))
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
have id : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
have id₁ : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
have id₂ : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
  (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)
id₂ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
have id₃ : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
  (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)
id₂ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
id₃ :
  ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
have id₄ : ((Hom.id one).comp Hom.leftCompReflexion).comp (Hom.id one) =
  (Hom.id one).comp (Hom.leftCompReflexion.comp (Hom.id one))
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
have id : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
have id₁ : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
have id₂ : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
  (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)
id₂ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
have id₃ : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
  (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
id : ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)
id₁ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)
id₂ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
id₃ :
  ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
have id₄ : ((Hom.id one).comp Hom.rightCompReflexion).comp (Hom.id one) =
  (Hom.id one).comp (Hom.rightCompReflexion.comp (Hom.id one))
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
Tactic: cases h
Cleared hypotheses: W, Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id₁ : ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)
Tactic: cases h
Cleared hypotheses: W, Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
id₁ : ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id₂ : ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)
Tactic: cases h
Cleared hypotheses: W, Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
id₁ : ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)
id₂ : ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id₃ : ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
  (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)
Tactic: cases h
Cleared hypotheses: W, Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
id₁ : ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)
id₂ : ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)
id₃ :
  ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id₄ : ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
  (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)
Tactic: cases h
Cleared hypotheses: W, Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Z : WalkingReflexivePair
h : W.Hom Z
id : ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)
id₁ : ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)
id₂ : ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)
id₃ :
  ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)
id₄ :
  ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)
⊢ ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
have id₅ : ((Hom.id W).comp (Hom.id W)).comp (Hom.id W) = (Hom.id W).comp ((Hom.id W).comp (Hom.id W))
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)
have rw : F.map (reflexion ≫ left) = 𝟙 (F.obj zero)
Tactic: rw [← F.map_comp, reflexion_comp_left, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ left) = 𝟙 (F.obj zero)
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)
have rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
Tactic: rw [← F.map_comp, reflexion_comp_left, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ left) = 𝟙 (F.obj zero)
rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)
have rw₂ : Eq.{v + 1} (α := F.obj zero ⟶ F.obj zero) (𝟙 (F.obj zero)) (𝟙 (F.obj zero))
Tactic: rw [← F.map_comp, reflexion_comp_left, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)
have rw : F.map (reflexion ≫ right) = 𝟙 (F.obj zero)
Tactic: rw [← F.map_comp, reflexion_comp_right, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ right) = 𝟙 (F.obj zero)
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)
have rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
Tactic: rw [← F.map_comp, reflexion_comp_right, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ right) = 𝟙 (F.obj zero)
rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)
have rw₂ : Eq.{v + 1} (α := F.obj zero ⟶ F.obj zero) (𝟙 (F.obj zero)) (𝟙 (F.obj zero))
Tactic: rw [← F.map_comp, reflexion_comp_right, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
⊢ Nonempty (StructuredArrow X inclusionWalkingReflexivePair)
have zero : Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
Tactic: cases X with
  | zero => exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩
  | one => exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
zero : Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
⊢ Nonempty (StructuredArrow X inclusionWalkingReflexivePair)
have one : Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
Tactic: cases X with
  | zero => exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩
  | one => exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
have zero : ∀ (p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)),
  StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p →
    (∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂),
        j₁ ∈ p ↔ j₂ ∈ p) →
      ∀ (j : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair), j ∈ p
Tactic: refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
have one : ∀ (p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair))
  (h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p)
  (h₂ :
    ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p)
  (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
Tactic: refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
have hₗ : StructuredArrow.mk (Y := one) left ∈ p
Tactic: have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
have hᵣ : StructuredArrow.mk (Y := one) right ∈ p
Tactic: have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)
have zero : IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
Tactic: cases X with
  | zero =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
      rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 h₁
      · exact h₁
  | one =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
      have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
      have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
      rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
      · exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
      all_goals assumption
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
zero : IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)
have one : IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
Tactic: cases X with
  | zero =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
      rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 h₁
      · exact h₁
  | one =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
      have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
      have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
      rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
      · exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
      all_goals assumption
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
h₂ : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
h₃ : F.map Hom.reflexion ≫ e₁ = e₀ ≫ G.map Hom.reflexion
x x_1 : WalkingReflexivePair
f : x ⟶ x_1
left :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.left ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.left)
right :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.right ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.right)
reflexion :
  Eq (α := F.obj zero ⟶ G.obj one)
    (F.map Hom.reflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.reflexion)
⊢ Eq (α := F.obj x ⟶ G.obj x_1)
    (F.map f ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x_1 with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map f)
have leftCompReflexion : Eq (α := F.obj one ⟶ G.obj one)
  (F.map leftCompReflexion ≫
    match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
    | zero => e₀
    | one => e₁)
  ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
    | zero => e₀
    | one => e₁) ≫
    G.map leftCompReflexion)
Tactic: cases f
Cleared hypotheses: x, x_1, f