Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 V
u v : V
h : Quot.mk (Sym2.Rel V) (u, v) ∈ G.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩)) =
    Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩

pp: case inr.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 W
u v : W
h : Quot.mk (Sym2.Rel W) (u, v) ∈ H.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩)) =
    Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩

Tactic:
<;>

Goal state after:
case inl.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 V
u v : V
h : Quot.mk (Sym2.Rel V) (u, v) ∈ G.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩)) =
    Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩

case inr.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 W
u v : W
h : Quot.mk (Sym2.Rel W) (u, v) ∈ H.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩)) =
    Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩