awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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)
refine :
  ∀ (c c' : γ) (h : (Prod.Lex rα rβ on fun (c : γ) ↦ (f c, g 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 (rβ on g) 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'
⊢ WellFounded.{u_4 + 1} (α := γ) (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 => ?_

Premises used: Iff.mpr, WellFounded.psigma_lex, Set.wellFoundedOn_range, WellFounded.onFun, WellFounded.mono, Subtype.val
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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'
inl :
  ∀ (h' : rα ((fun (c : γ) ↦ (f c, g c)) c).1 ((fun (c : γ) ↦ (f c, g c)) c').1),
    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 (rβ on g) 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_2 + 1} (α := α) ((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),
    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 (rβ on g) 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 (rβ on g) 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' := Prod.lex_iff.1 h

Premises used: Prod.lex_iff, Iff.mp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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
⊢ 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 (rβ on g) 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:
PSigma.Lex.left _ _ h'

Premises used: PSigma.Lex.left
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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
⊢ 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 (rβ on g) 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:
exact PSigma.Lex.left _ _ h'

Premises used: PSigma.Lex.left
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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' :
  Eq.{u_2 + 1} (α := α) ((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
inr :
  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 (rβ on g) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : α)})
    (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 ⁻¹' {f c}) 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 ⁻¹' {f 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 (rβ on g) 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:
dsimp only [InvImage, (· on ·)] at h' ⊢

Premises used: Function.onFun, InvImage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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 : { x : α // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : α)} })
    (Subrel rα fun (x : α) ↦ x ∈ range f)
    (fun (a : { x : α // x ∈ range f }) ↦ Subrel (rβ on g) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : α)})
    (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 ⋯))
    (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 ⁻¹' {f c'}) c' ⋯))

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

Premises used: PSigma.Lex.right, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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')
h₁ :
  Eq (α := (a : { x : α // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : α)} })
    (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 ⁻¹' {f c}) 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 ⋯))
inr : { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') ⋯) : α)} }
inr₁ :
  Subrel (rβ on g) (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(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 ⋯)
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' ⋯)
⊢ 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 (rβ on g) fun (x : γ) ↦ x ∈ f ⁻¹' {(↑a : α)})
    (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 ⁻¹' {f c}) 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 ⁻¹' {f c'}) c' ⋯))

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

Premises used: PSigma.Lex.right, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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')
⊢ Eq (α := (a : { x : α // x ∈ range f }) ×' { x : γ // x ∈ f ⁻¹' {(↑a : α)} })
    (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 ⁻¹' {f c}) 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 ⋯))

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

Premises used: PSigma.subtype_ext, And.left, rfl, Subtype.ext
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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')
⊢ Subrel (rβ on g) (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(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 ⋯)
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' ⋯)

Tactic:
h'.2

Premises used: Subrel, And.right, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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')
⊢ { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') ⋯) : α)} }

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

Premises used: PSigma.subtype_ext, And.right, rfl, Subtype.ext
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : s.WellFoundedOn (rα on f)
hβ : ∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (rβ on g)
⊢ s.WellFoundedOn (Prod.Lex rα rβ on fun (c : γ) ↦ (f c, g c))

Tactic:
WellFounded.prod_lex_of_wellFoundedOn_fiber hα
    fun a ↦ ((hβ a).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun _ _ h ↦ ‹_›)

Premises used: Subrel, WellFounded.onFun, WellFounded.mono, WellFounded.prod_lex_of_wellFoundedOn_fiber, Order.Preimage, Set.WellFoundedOn
-- 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)
⊢ WellFounded.{u_4 + 1} (α := γ)
    (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) c))

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

Premises used: Iff.mpr, WellFounded.psigma_lex, Set.wellFoundedOn_range, WellFounded.onFun, WellFounded.mono, Subtype.val
-- 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)
refine :
  ∀ (c c' : γ)
    (h : (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (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'
⊢ WellFounded.{u_4 + 1} (α := γ)
    (Sigma.Lex (α := π) rι rπ on fun (c : γ) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) (f c) (g (f c) 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 => ?_

Premises used: Iff.mpr, WellFounded.psigma_lex, Set.wellFoundedOn_range, WellFounded.onFun, WellFounded.mono, Subtype.val
-- 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'
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'

Tactic:
PSigma.Lex.left _ _ h'

Premises used: PSigma.Lex.left
-- 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'
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'

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

Premises used: PSigma.Lex.left
-- 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'
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'))
inr :
  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 : ι)})
    (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 ⁻¹' {f c}) 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 ⁻¹' {f 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:
dsimp only [InvImage, (· on ·)] at h' ⊢

Premises used: Function.onFun, InvImage
-- 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'
h' : f c = f 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'))
⊢ 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 : ι)})
    (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 h'))
    (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 ⁻¹' {f c'}) c' ⋯))

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

Premises used: PSigma.Lex.right, Subtype.mk, Exists.intro, rfl