-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem smaller_mono {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) : smaller C o₁ ⊆ smaller C o₂

Proof state:
case h.intro.mk
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x => ord I x < o₂) ∧
    (πs C o₂) ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) =
      (πs C o₁) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Tactic:
refine ⟨?_, ?_⟩

Result:
case h.intro.mk.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x => ord I x < o₂)

case h.intro.mk.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) =
    (πs C o₁) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Proof state:
case h.intro.mk.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ ((eval (π C fun x => ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestrict C fun x => ord I x < o₁) =
    ⇑(eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∘ ProjRestrict C fun x => ord I x < o₁

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ (πs C o₁) g ∈ smaller C o₂

Tactic:
simp only [smaller, Set.mem_image]

Result:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ ∃ x ∈ range (π C fun x => ord I x < o₂), (πs C o₂) x = (πs C o₁) g

Proof state:
case h.intro.mk.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) =
    (πs C o₁) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Tactic:
rw [← LocallyConstant.coe_inj, coe_πs C o₂, ← LocallyConstant.toFun_eq_coe, coe_πs',
  Function.comp_assoc, projRestricts_comp_projRestrict C _, coe_πs]

Result:
case h.intro.mk.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ ((eval (π C fun x => ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestrict C fun x => ord I x < o₁) =
    ⇑(eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∘ ProjRestrict C fun x => ord I x < o₁

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
x : ↑(π C fun x => ord I x < o₂)
⊢ (eval (π C fun x => ord I x < o₂) ⟨l, ⋯⟩) x = ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) x

Tactic:
rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood  C _ gl), eval]

Result:
no goals

Proof state:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ ∃ x ∈ range (π C fun x => ord I x < o₂), (πs C o₂) x = (πs C o₁) g

Tactic:
use πs' C h g

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ (πs' C h) g ∈ range (π C fun x => ord I x < o₂) ∧ (πs C o₂) ((πs' C h) g) = (πs C o₁) g

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ (πs' C h) g ∈ range (π C fun x => ord I x < o₂) ∧ (πs C o₂) ((πs' C h) g) = (πs C o₁) g

Tactic:
obtain ⟨⟨l, gl⟩, rfl⟩ := hg

Result:
case h.intro.mk
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x => ord I x < o₂) ∧
    (πs C o₂) ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) =
      (πs C o₁) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
⊢ smaller C o₁ ⊆ smaller C o₂

Tactic:
rintro f ⟨g, hg, rfl⟩

Result:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
hg : g ∈ range (π C fun x => ord I x < o₁)
⊢ (πs C o₁) g ∈ smaller C o₂

Proof state:
case h.intro.mk.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x => ord I x < o₂)

Tactic:
use ⟨l, Products.isGood_mono C h gl⟩

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ eval (π C fun x => ord I x < o₂) ⟨l, ⋯⟩ = (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
⊢ eval (π C fun x => ord I x < o₂) ⟨l, ⋯⟩ = (πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)

Tactic:
ext x

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x => ord I x < o₁) l
x : ↑(π C fun x => ord I x < o₂)
⊢ (eval (π C fun x => ord I x < o₂) ⟨l, ⋯⟩) x = ((πs' C h) (eval (π C fun x => ord I x < o₁) ⟨l, gl⟩)) x