-- Mathlib/Order/WellFoundedSet.lean
theorem WellFounded.prod_lex_of_wellFoundedOn_fiber (hα : WellFounded (rα on f))
    (hβ : ∀ a, (f ⁻¹' {a}).WellFoundedOn (rβ on g)) :
    WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
⊢ WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))

Tactic:
refine ((psigma_lex (wellFoundedOn_range.2 hα) fun a => hβ a).onFun
  (f := fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩)).mono fun c c' h => ?_

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

Proof state:
case inr.convert_4
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case h.e'_5.h
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

case inr.convert_6
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?inr.convert_4) (g ↑⟨c', ⋯⟩)

Tactic:
exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : rα ((fun c => (f c, g c)) c).1 ((fun c => (f c, g c)) c').1
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

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

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

Tactic:
obtain h' | h' := Prod.lex_iff.1 h

Result:
case inl
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : rα ((fun c => (f c, g c)) c).1 ((fun c => (f c, g c)) c').1
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' :
  ((fun c => (f c, g c)) c).1 = ((fun c => (f c, g c)) c').1 ∧
    rβ ((fun c => (f c, g c)) c).2 ((fun c => (f c, g c)) c').2
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'

Proof state:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ PSigma.Lex (fun a b => rα ↑a ↑b) (fun a a_1 b => rβ (g ↑a_1) (g ↑b)) ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ ⟨⟨f c', ⋯⟩, ⟨c', ⋯⟩⟩

Tactic:
convert PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1

Result:
case h.e'_5.h
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

case inr.convert_4
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case inr.convert_6
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?inr.convert_4) (g ↑⟨c', ⋯⟩)

Proof state:
case h.e'_5.h
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

case inr.convert_4
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case inr.convert_6
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?inr.convert_4) (g ↑⟨c', ⋯⟩)

Tactic:
swap

Result:
case inr.convert_4
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑⟨f c', ⋯⟩})

case h.e'_5.h
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

case inr.convert_6
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?inr.convert_4) (g ↑⟨c', ⋯⟩)