Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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
⊢ Function.LeftInverse
    (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⟩) ⋯)
    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 ⋯)
        ⋯

Tactic:
rintro ⟨⟨u | u, v | v⟩, h⟩

Goal state after:
case mk.inl.inl
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 ⊕ W)
u v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (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⟩) ⋯)
      ((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 ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩

case mk.inl.inr
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 ⊕ W)
u : V
v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (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⟩) ⋯)
      ((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 ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v), h⟩

case mk.inr.inl
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 ⊕ W)
u : W
v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (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⟩) ⋯)
      ((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 ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v), h⟩

case mk.inr.inr
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 ⊕ W)
u v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (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⟩) ⋯)
      ((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 ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩