awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
h₁ :
  Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
    (range (π C fun (x : I) ↦ ord I x < o₂))
    ((πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
h₂ :
  Eq (α := LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₂ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
      LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₁ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑C : Type u) ℤ)
⊢ Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (range (π C fun (x : I) ↦ ord I x < o₂))
      ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ∧
    Eq (α := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₂ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          ((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (eval (π C fun (x : I) ↦ ord I x < o₁)
              (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
        LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₁ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        LocallyConstant (↑C : Type u) ℤ)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
h₁ :
  eval (π C fun (x : I) ↦ ord I x < o₂)
      (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) =
    (πs' C h :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < o₁)
        (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))
⊢ Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
    (range (π C fun (x : I) ↦ ord I x < o₂))
    ((πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)

Tactic:
use ⟨l, Products.isGood_mono C h gl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
h₁ :
  ∀ (x : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)),
    Eq (α := ℤ)
      ((eval (π C fun (x : I) ↦ ord I x < o₂)
              (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
            (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
          x :
        ℤ)
      ((((πs' C h :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                    LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
                (eval (π C fun (x : I) ↦ ord I x < o₁)
                  (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
            (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
          x :
        ℤ)
⊢ eval (π C fun (x : I) ↦ ord I x < o₂)
      (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) =
    (πs' C h :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < o₁)
        (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
h₁ :
  ((eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)).toFun ∘
      ProjRestrict C fun (x : I) ↦ ord I x < o₁) =
    Function.comp (β := (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u))
      (⇑(eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u)) → ℤ)
      (ProjRestrict C fun (x : I) ↦ ord I x < o₁)
⊢ Eq (α := LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₂ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
      LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₁ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑C : Type u) ℤ)

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

Premises used: Profinite.NobelingProof.projRestricts_comp_projRestrict, Profinite.NobelingProof.coe_πs, LocallyConstant.coe_inj, LocallyConstant.toFun_eq_coe, Profinite.NobelingProof.coe_πs', Function.comp_assoc
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
⊢ ((eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)).toFun ∘
      ProjRestrict C fun (x : I) ↦ ord I x < o₁) =
    Function.comp (β := (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u))
      (⇑(eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u)) → ℤ)
      (ProjRestrict C fun (x : I) ↦ ord I x < o₁)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
⊢ isGood (π C fun (x : I) ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l

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

Premises used: Profinite.NobelingProof.Products.isGood, Profinite.NobelingProof.π, le_of_lt, Profinite.NobelingProof.ord, LT.lt, Iff.intro, _private.0.Profinite.NobelingProof.Products.limitOrdinal.match_1, Profinite.NobelingProof.Products.isGood_mono
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
refine : ∀ (h : isGood (π C fun (x : I) ↦ ord I x < o) l), ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l
⊢ isGood (π C fun (x : I) ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
h₁ :
  ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l
⊢ ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l

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

Premises used: Order.succ, List.toFinset, Profinite.NobelingProof.ord, Finset.sup, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
simp : ∀ b ∈ (↑l : List I), Order.succ (ord I b) < o
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o

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

Premises used: List.mem_toFinset, Finset.sup_lt_iff, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ∀ b ∈ (↑l : List I), Order.succ (ord I b) < o

Tactic:
fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)

Premises used: Order.IsSuccLimit.succ_lt, Profinite.NobelingProof.ord, Profinite.NobelingProof.Products.prop_of_isGood, LT.lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ∀ b ∈ (↑l : List I), Order.succ (ord I b) < o

Tactic:
exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)

Premises used: Order.IsSuccLimit.succ_lt, Profinite.NobelingProof.ord, Profinite.NobelingProof.Products.prop_of_isGood, LT.lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o

Tactic:
have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o := by
    simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
    exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l

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

Premises used: And.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
h₁ :
  ∀
    (he :
      Membership.mem (γ :=
        Submodule ℤ
          (LocallyConstant
            (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
        (Submodule.span ℤ
          (Set.image (α := Products I)
            (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
            {m : Products I | m < l}))
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)),
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
      (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o) l)
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l

Tactic:
refine ⟨hslt, fun he ↦ h ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
i : I
hi : i ∈ (↑l : List I)
simp : ∃ b ∈ (↑l : List I), ord I i ≤ ord I b
⊢ ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)

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

Premises used: List.mem_toFinset, Order.lt_succ_iff, Finset.lt_sup_iff
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
i : I
hi : i ∈ (↑l : List I)
⊢ ∃ b ∈ (↑l : List I), ord I i ≤ ord I b

Tactic:
⟨i, hi, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
i : I
hi : i ∈ (↑l : List I)
⊢ ∃ b ∈ (↑l : List I), ord I i ≤ ord I b

Tactic:
exact ⟨i, hi, le_rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
⊢ ∀ i ∈ (↑l : List I), ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)

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⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
h :
  ∀ (p : LocallyConstant (↑C : Type u) ℤ),
    p ∈ range C ↔
      Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
        (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) p
⊢ range C = ⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})

Tactic:
ext p
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
h :
  (∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p
⊢ p ∈ range C ↔
    Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
      (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) p

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

Premises used: Profinite.NobelingProof.GoodProducts.smaller, Set.mem_range, Set.mem_iUnion, Set.mem_image, Subtype.exists, Profinite.NobelingProof.GoodProducts.range
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
⊢ (∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p

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

Premises used: Iff.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
h :
  ∀
    (hp :
      ∃ (a : Products I) (b : Products.isGood C a),
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p),
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p
h₁ :
  ∀
    (hp :
      ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
        (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
            eval (π C fun (x : I) ↦ ord I x < a)
                (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
              x) ∧
          (πs C a :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              x =
            p),
    ∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p
⊢ (∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p

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