-- Mathlib/Order/WellFoundedSet.lean
theorem WellFounded.sigma_lex_of_wellFoundedOn_fiber (hι : WellFounded (rι on f))
    (hπ : ∀ i, (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)) :
    WellFounded (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)

Proof state:
case h.e'_5.h
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.intro.convert_4⟩

case inr.intro.convert_4
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case inr.intro.convert_6
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ rπ (↑⟨f c', ⋯⟩) (g ↑⟨f c', ⋯⟩ ↑?inr.intro.convert_4) (g ↑⟨f c', ⋯⟩ ↑⟨c', ⋯⟩)

Tactic:
swap

Result:
case inr.intro.convert_4
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case h.e'_5.h
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.intro.convert_4⟩

case inr.intro.convert_6
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ rπ (↑⟨f c', ⋯⟩) (g ↑⟨f c', ⋯⟩ ↑?inr.intro.convert_4) (g ↑⟨f c', ⋯⟩ ↑⟨c', ⋯⟩)

Proof state:
ι : 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 => ⟨f c, g (f c) c⟩) c c'
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

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

Result:
case inl
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : rι ((fun c => ⟨f c, g (f c) c⟩) c).fst ((fun c => ⟨f c, g (f c) c⟩) c').fst
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

case inr.intro
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : ((fun c => ⟨f c, g (f c) c⟩) c).fst = ((fun c => ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

Proof state:
case inr.intro.convert_4
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

Tactic:
exact ⟨c, h'⟩

Result:
no goals

Proof state:
case inr.intro.convert_6
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h'' : rπ (f c') (⋯ ▸ g (f c') c) (g (f c') c')
⊢ rπ (f c') (g (f c') c) (g (f c') c')

Tactic:
exact h''

Result:
no goals

Proof state:
case inl
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : rι ((fun c => ⟨f c, g (f c) c⟩) c).fst ((fun c => ⟨f c, g (f c) c⟩) c').fst
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

Tactic:
exact PSigma.Lex.left _ _ h'

Result:
no goals

Proof state:
case inr.intro.convert_6
ι : 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 => ⟨f c, g (f c) c⟩) c c'
⊢ ∀ (h' : f c = f c'), rπ (f c') (h' ▸ g (f c) c) (g (f c') c') → rπ (f c') (g (f c') c) (g (f c') c')

Tactic:
generalize f c = d

Result:
case inr.intro.convert_6
ι : 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 => ⟨f c, g (f c) c⟩) c c'
d : ι
⊢ ∀ (h' : d = f c'), rπ (f c') (h' ▸ g d c) (g (f c') c') → rπ (f c') (g (f c') c) (g (f c') c')

Proof state:
case h.e'_5.h
ι : 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 => ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd)
    ((fun c => ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩

Tactic:
exact PSigma.subtype_ext (Subtype.ext h') rfl

Result:
no goals