-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem eval_πs_image' {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂)
    (hl : ∀ i ∈ l.val, ord I i < o₁) : eval (π C (ord I · < o₂)) '' { m | m < l } =
    (πs' C h) '' (eval (π C (ord I · < o₁)) '' { m | m < l })

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
⊢ eval (π C fun x => ord I x < o₂) '' {m | m < l} = ⇑(πs' C h) '' (eval (π C fun x => ord I x < o₁) '' {m | m < l})

Tactic:
ext f

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ f ∈ eval (π C fun x => ord I x < o₂) '' {m | m < l} ↔
    f ∈ ⇑(πs' C h) '' (eval (π C fun x => ord I x < o₁) '' {m | m < l})

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
⊢ m < l ∧ eval (π C fun x => ord I x < o₂) m = f ↔ m < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f

Tactic:
apply and_congr_right

Result:
case h.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
⊢ m < l → (eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f)

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ ∀ (a : Products I),
    a < l ∧ eval (π C fun x => ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f

Tactic:
intro m

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
⊢ m < l ∧ eval (π C fun x => ord I x < o₂) m = f ↔ m < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f

Proof state:
case h.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
hm : m < l
⊢ eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f

Tactic:
rw [eval_πs' C h (lt_ord_of_lt hm hl)]

Result:
no goals

Proof state:
case h.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
⊢ m < l → (eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f)

Tactic:
intro hm

Result:
case h.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
m : Products I
hm : m < l
⊢ eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ (∃ x < l, eval (π C fun x => ord I x < o₂) x = f) ↔ ∃ a < l, (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f

Tactic:
apply exists_congr

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ ∀ (a : Products I),
    a < l ∧ eval (π C fun x => ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ f ∈ eval (π C fun x => ord I x < o₂) '' {m | m < l} ↔
    f ∈ ⇑(πs' C h) '' (eval (π C fun x => ord I x < o₁) '' {m | m < l})

Tactic:
simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ
⊢ (∃ x < l, eval (π C fun x => ord I x < o₂) x = f) ↔ ∃ a < l, (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f