-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c c'
inl :
  ∀
    (h' :
      rι (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
        (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))),
    Function.onFun (β := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (PSigma.Lex (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
        (Subrel rι fun (x : ι) ↦ x ∈ range f) fun (a : { x : ι // x ∈ range f }) ↦
        Subrel (Function.onFun (β := π (↑a : ι)) (rπ (↑a : ι)) (g (↑a : ι))) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : ι)})
      (fun (c : γ) ↦
        PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯)
          (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) : ι)}) c
            ⋯))
      c c'
inr :
  ∀
    (h' :
      Eq.{u_1 + 1} (α := ι)
        (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
        (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c')))
    (h'' :
      rπ (Sigma.fst (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))
        (Eq.rec (motive :=
          fun (x : ι)
            (x_1 :
              Sigma.fst (β := fun (i : ι) ↦ π i)
                  ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c) =
                x) ↦
          π x)
          (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c))
          h')
        (Sigma.snd (β := fun (i : ι) ↦ π i) ((fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c)) c'))),
    Function.onFun (β := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (PSigma.Lex (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
        (Subrel rι fun (x : ι) ↦ x ∈ range f) fun (a : { x : ι // x ∈ range f }) ↦
        Subrel (Function.onFun (β := π (↑a : ι)) (rπ (↑a : ι)) (g (↑a : ι))) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : ι)})
      (fun (c : γ) ↦
        PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯)
          (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) : ι)}) c
            ⋯))
      c c'
⊢ Function.onFun (β := (a : { x : ι // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (PSigma.Lex (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
      (Subrel rι fun (x : ι) ↦ x ∈ range f) fun (a : { x : ι // x ∈ range f }) ↦
      Subrel (Function.onFun (β := π (↑a : ι)) (rπ (↑a : ι)) (g (↑a : ι))) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : ι)})
    (fun (c : γ) ↦
      PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) ⋯) : ι)}) c ⋯))
    c c'

Tactic:
obtain h' | ⟨h', h''⟩ := Sigma.lex_iff.1 h

Premises used: Sigma.lex_iff, Iff.mp