Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x y z : WalkingIso
x✝¹ : x ⟶ y
x✝ : y ⟶ z
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) z x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) z x)
      x (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ y) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) y x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) y x)
        x x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) z x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) z x)
        y x✝

Tactic:
induction x

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y z : WalkingIso
x✝¹ : y ⟶ z
x✝ : zero ⟶ y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) z x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) z x)
      zero (x✝ ≫ x✝¹) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ y) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) y x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) y x)
        zero x✝ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) z x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) z x)
        y x✝¹

case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y z : WalkingIso
x✝¹ : y ⟶ z
x✝ : one ⟶ y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) z x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) z x)
      one (x✝ ≫ x✝¹) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ y) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y y))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) y x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) y x)
        one x✝ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ z) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y z))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) z x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) z x)
        y x✝¹