-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.limitOrdinal (l : Products I) : l.isGood (π C (ord I · < o)) ↔
    ∃ (o' : Ordinal), o' < o ∧ l.isGood (π C (ord I · < o'))

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
⊢ ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o ∧
    isGood (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l

Tactic:
refine ⟨hslt, fun he ↦ h ?_⟩

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
⊢ eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)
⊢ eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})

Tactic:
rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
  Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
⊢ ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)

Tactic:
intro i hi

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
i : I
hi : i ∈ ↑l
⊢ ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
⊢ isGood (π C fun x => ord I x < o) l ↔ ∃ o' < o, isGood (π C fun x => ord I x < o') l

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩

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

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
i : I
hi : i ∈ ↑l
⊢ ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)

Tactic:
simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
i : I
hi : i ∈ ↑l
⊢ ∃ b ∈ ↑l, ord I i ≤ ord I b

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
⊢ eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})

Tactic:
have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) := by
  intro i hi
  simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
  exact ⟨i, hi, le_rfl⟩

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)
⊢ eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
⊢ ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o

Tactic:
simp only [Finset.sup_lt_iff ho.pos, List.mem_toFinset]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
⊢ ∀ b ∈ ↑l, Order.succ (ord I b) < o

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o
he :
  eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})
i : I
hi : i ∈ ↑l
⊢ ∃ b ∈ ↑l, ord I i ≤ ord I b

Tactic:
exact ⟨i, hi, le_rfl⟩

Result:
no goals

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

Tactic:
use Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a))

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
l : Products I
h : isGood (π C fun x => ord I x < o) l
⊢ ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o ∧
    isGood (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l