awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b : Lex (α × β)
hb :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) b
c : Lex (α × β)
hc :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) c
hbc : b ≤ c
hb₁ : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
⊢ f b ≤ f c
have hc₁ : ((ofLex : (a : Lex (α × β)) → α × β) c).1 = a
Tactic: simp only [mem_preimage, mem_singleton_iff] at hb hc
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
hc : ((ofLex : (a : Lex (α × β)) → α × β) c).1 = a
⊢ f b ≤ f c
have this : LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∨
  Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) b).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1 ∧ f b ≤ f c
Tactic: have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c :=
    Prod.Lex.toLex_le_toLex.mp hbc
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
⊢ WellFounded.{u_4 + 1} (α := γ) (Prod.Lex rα rβ on fun (c : γ) ↦ (f c, g c))
have 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) sorry)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) sorry) : α)}) c sorry))
    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 => ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'
⊢ 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'
have 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) sorry)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) sorry) : α)}) c sorry))
    c c'
Tactic: obtain h' | h' := Prod.lex_iff.1 h
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'
⊢ 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'
have 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) sorry)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) sorry) : α)}) c sorry))
    c c'
Tactic: obtain h' | h' := Prod.lex_iff.1 h
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ 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'
have 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) sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c sorry))
  (PSigma.mk (β := fun (a : { x : α // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : α)} })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' sorry))
Tactic: dsimp only [InvImage, (· on ·)] at h' ⊢
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 ⁻¹' {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' ⋯))
have 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) sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c sorry))
  (PSigma.mk (β := fun (a : { x : α // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : α)} })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry)
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry) : α)}) c sorry))
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 ⋯))
⊢ 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' ⋯))
have inr : { x : γ // x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry) : α)} }
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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') ⋯) : α)} }
⊢ 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' ⋯))
have inr₁ : Subrel (rβ on g) (fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry) : α)})
  (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') sorry) : α)}) c sorry)
  (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' sorry)
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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))
have 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) sorry)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) sorry) : ι)}) c sorry))
    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 => ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'
⊢ 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'
have 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) sorry)
        (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c) sorry) : ι)}) c sorry))
    c c'
Tactic: obtain h' | ⟨h', h''⟩ := Sigma.lex_iff.1 h
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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'))
⊢ 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'
have 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) sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c sorry))
  (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c'}) c' sorry))
Tactic: dsimp only [InvImage, (· on ·)] at h' ⊢
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 ⁻¹' {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' ⋯))
have 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) sorry) (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {f c}) c sorry))
  (PSigma.mk (β := fun (a : { x : ι // x ∈ range f }) ↦ { x : γ // x ∈ f ⁻¹' {(↑a : ι)} })
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry)
    (Subtype.mk (p := fun (x : γ) ↦ x ∈ f ⁻¹' {(↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ range f) (f c') sorry) : ι)}) c h'))
Tactic: convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1