-- Mathlib/Order/WellFoundedSet.lean
theorem fiberProdLex [PartialOrder α] [Preorder β] {s : Set (α ×ₗ β)}
    (hαβ : s.IsPWO) (a : α) : {y | toLex (a, y) ∈ s}.IsPWO

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
rw [h]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ (f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})).IsPWO

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ MonotoneOn f (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})

Tactic:
rintro b ⟨-, hb⟩ c ⟨-, hc⟩ hbc

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b : Lex (α × β)
hb : b ∈ (fun x => (ofLex x).1) ⁻¹' {a}
c : Lex (α × β)
hc : c ∈ (fun x => (ofLex x).1) ⁻¹' {a}
hbc : b ≤ c
⊢ f b ≤ f c

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
x : β
⊢ x ∈ {y | toLex (a, y) ∈ s} ↔ x ∈ f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})

Tactic:
simp [f]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ (f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})).IsPWO

Tactic:
apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)

Result:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ MonotoneOn f (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a}) := by
  ext x
  simp [f]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
let f : α ×ₗ β → β := fun x => (ofLex x).2

Result:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
⊢ {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})

Tactic:
ext x

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
x : β
⊢ x ∈ {y | toLex (a, y) ∈ s} ↔ x ∈ f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
this : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c
⊢ f b ≤ f c

Tactic:
simp_all only [lt_self_iff_false, true_and, false_or]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b : Lex (α × β)
hb : b ∈ (fun x => (ofLex x).1) ⁻¹' {a}
c : Lex (α × β)
hc : c ∈ (fun x => (ofLex x).1) ⁻¹' {a}
hbc : b ≤ c
⊢ f b ≤ f c

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hb hc

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
⊢ f b ≤ f c

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
⊢ 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

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x => (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
this : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c
⊢ f b ≤ f c