-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.union : range C = ⋃ (e : {o' // o' < o}), (smaller C e.val)

Proof state:
case h.refine_1.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl✝ : Products.isGood C l
hl : ∃ o' < o, Products.isGood (π C fun x => ord I x < o') l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl✝⟩

Tactic:
obtain ⟨o', ho'⟩ := hl

Result:
case h.refine_1.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl : Products.isGood C l
o' : Ordinal.{u}
ho' : o' < o ∧ Products.isGood (π C fun x => ord I x < o') l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl⟩

Proof state:
case h.refine_1.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl : Products.isGood C l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl⟩

Tactic:
rw [contained_eq_proj C o hsC, Products.limitOrdinal C ho] at hl

Result:
case h.refine_1.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl✝ : Products.isGood C l
hl : ∃ o' < o, Products.isGood (π C fun x => ord I x < o') l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl✝⟩

Proof state:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ Products.isGood (π C fun x => ord I x < o) l

Tactic:
exact Products.isGood_mono C (le_of_lt h) hl

Result:
no goals

Proof state:
case h.refine_1.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl : Products.isGood C l
o' : Ordinal.{u}
ho' : o' < o ∧ Products.isGood (π C fun x => ord I x < o') l
⊢ (πs C o') (eval (π C fun x => ord I x < o') ⟨l, ⋯⟩) = eval C ⟨l, hl⟩

Tactic:
exact Products.eval_πs C (Products.prop_of_isGood  C _ ho'.2)

Result:
no goals

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ (∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p) ↔
    ∃ a,
      ∃ (h : a < o),
        ∃ x,
          (∃ a_1,
              ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
            (πs C a) x = p

Tactic:
refine ⟨fun hp ↦ ?_, fun hp ↦ ?_⟩

Result:
case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp : ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p

case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp :
  ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p
⊢ ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p

Proof state:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp :
  ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p
⊢ ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p

Tactic:
obtain ⟨o', h, _, ⟨l, hl, rfl⟩, rfl⟩ := hp

Result:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = (πs C o') (eval (π C fun x => ord I x < o') ⟨l, ⋯⟩)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ p ∈ range C ↔ p ∈ ⋃ e, smaller C ↑e

Tactic:
simp only [smaller, range, Set.mem_iUnion, Set.mem_image, Set.mem_range, Subtype.exists]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ (∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p) ↔
    ∃ a,
      ∃ (h : a < o),
        ∃ x,
          (∃ a_1,
              ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
            (πs C a) x = p

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
⊢ range C = ⋃ e, smaller C ↑e

Tactic:
ext p

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ p ∈ range C ↔ p ∈ ⋃ e, smaller C ↑e

Proof state:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = (πs C o') (eval (π C fun x => ord I x < o') ⟨l, ⋯⟩)

Tactic:
refine ⟨l, ?_, (Products.eval_πs C (Products.prop_of_isGood  C _ hl)).symm⟩

Result:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ Products.isGood C l

Proof state:
case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp : ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p

Tactic:
obtain ⟨l, hl, rfl⟩ := hp

Result:
case h.refine_1.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
l : Products I
hl : Products.isGood C l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1,
            ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl⟩