awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (sum_to C ho) =
    GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho
have this : Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
    (sum_to C ho) =
  Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u))
      (Subtype.val (p := fun (x : Products I) ↦
        Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x)) ∪
    Set.range (ι := (↑(MaxProducts C ho) : Type u)) (Subtype.val (p := fun (x : Products I) ↦ x ∈ MaxProducts C ho))
Tactic: have : Set.range (sum_to C ho) = _ ∪ _ := Set.Sum.elim_range _ _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC_1 : contained C (Order.succ o)
ho_1 : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (sum_to C ho) =
    GoodProducts C
have rw : GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho = GoodProducts C
Tactic: rw [sum_to_range C ho, union_succ C hsC ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC_1 : contained C (Order.succ o)
ho_1 : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
rw : GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho = GoodProducts C
⊢ Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (sum_to C ho) =
    GoodProducts C
have rw₁ : GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho =
  GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho
Tactic: rw [sum_to_range C ho, union_succ C hsC ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ eval C ∘ (sum_equiv C hsC ho).toFun =
    Sum.elim (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)
have h : ∀ (val : Products I)
  (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
  (x : (↑C : Type u)),
  Eq (α := ℤ)
    (((eval C ∘ (sum_equiv C hsC ho).toFun)
            (Sum.inl
              (Subtype.mk (p := fun (x : Products I) ↦
                Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                property)) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
    ((Sum.elim
            (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
            (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
            (Sum.inl
              (Subtype.mk (p := fun (x : Products I) ↦
                Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                property)) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h :
  ∀ (val : Products I)
    (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
    (x : (↑C : Type u)),
    Eq (α := ℤ)
      (((eval C ∘ (sum_equiv C hsC ho).toFun)
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
⊢ eval C ∘ (sum_equiv C hsC ho).toFun =
    Sum.elim (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)
have h₁ : ∀ (val : (↑(MaxProducts C ho) : Type u)) (x : (↑C : Type u)),
  Eq (α := ℤ) (((eval C ∘ (sum_equiv C hsC ho).toFun) (Sum.inr val) : (a : (↑C : Type u)) → ℤ) x : ℤ)
    ((Sum.elim
            (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
            (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) (Sum.inr val) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ eval C ∘ (sum_equiv C hsC ho).toFun =
    Sum.elim (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)
have h : ∀ (val : Products I)
  (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
  (x : (↑C : Type u)),
  Eq (α := ℤ)
    (((eval C ∘ (sum_equiv C hsC ho).toFun)
            (Sum.inl
              (Subtype.mk (p := fun (x : Products I) ↦
                Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                property)) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
    ((Sum.elim
            (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
            (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
            (Sum.inl
              (Subtype.mk (p := fun (x : Products I) ↦
                Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                property)) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext ⟨_, _⟩ <;> [rfl; rfl]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h :
  ∀ (val : Products I)
    (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
    (x : (↑C : Type u)),
    Eq (α := ℤ)
      (((eval C ∘ (sum_equiv C hsC ho).toFun)
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
⊢ eval C ∘ (sum_equiv C hsC ho).toFun =
    Sum.elim (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)
have h₁ : ∀ (val : (↑(MaxProducts C ho) : Type u)) (x : (↑C : Type u)),
  Eq (α := ℤ) (((eval C ∘ (sum_equiv C hsC ho).toFun) (Sum.inr val) : (a : (↑C : Type u)) → ℤ) x : ℤ)
    ((Sum.elim
            (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
            (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) (Sum.inr val) :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext ⟨_, _⟩ <;> [rfl; rfl]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C) ↔
    LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      ℤ (SumEval C ho)
have rw : LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u)) ℤ
    (Function.comp (β := (↑(GoodProducts C) : Type u)) (eval C)
      (⇑(sum_equiv C hsC ho) :
        (a : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u)) →
          (↑(GoodProducts C) : Type u))) ↔
  LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)
Tactic: rw [← linearIndependent_equiv (sum_equiv C hsC ho), SumEval,
    ← sum_equiv_comp_eval_eq_elim C hsC ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
    Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (Sum.elim
        (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
        fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
have rw : Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) = Set.range (eval C ∘ (sum_equiv C hsC ho).toFun)
Tactic: rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
    EquivLike.range_comp (e := sum_equiv C hsC ho)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
rw :
  Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) = Set.range (eval C ∘ (sum_equiv C hsC ho).toFun)
⊢ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
    Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (Sum.elim
        (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
        fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
have rw₁ : Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
  Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
    (Function.comp (β := { l : Products I // Products.isGood C l }) (eval C)
      (⇑(sum_equiv C hsC ho) :
        (a : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u)) →
          (↑(GoodProducts C) : Type u)))
Tactic: rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
    EquivLike.range_comp (e := sum_equiv C hsC ho)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
rw :
  Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) = Set.range (eval C ∘ (sum_equiv C hsC ho).toFun)
rw₁ :
  Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
    Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (Function.comp (β := { l : Products I // Products.isGood C l }) (eval C)
        (⇑(sum_equiv C hsC ho) :
          (a : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u)) →
            (↑(GoodProducts C) : Type u)))
⊢ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
    Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (Sum.elim
        (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
        fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
have rw₂ : Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
  Set.range (ι := (↑(GoodProducts C) : Type u)) (eval C)
Tactic: rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
    EquivLike.range_comp (e := sum_equiv C hsC ho)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ SumEval C ho ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
            (ModuleCat.ofHom (πs C o))) :
        (a : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)) →
          (↑(ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ)) : Type u)) ∘
      eval (π C fun (x : I) ↦ ord I x < o)
have h : ∀ (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) (x : (↑C : Type u)),
  Eq (α := ℤ) (((SumEval C ho ∘ Sum.inl) l : (a : (↑C : Type u)) → ℤ) x : ℤ)
    ((((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (X :=
                    ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
                    (ModuleCat.ofHom (πs C o))) :
                (a : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)) →
                  (↑(ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ)) : Type u)) ∘
              eval (π C fun (x : I) ↦ ord I x < o))
            l :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext l
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
x : (↑C : Type u)
⊢ Eq (α := ℤ) (((SumEval C ho ∘ Sum.inl) l : (a : (↑C : Type u)) → ℤ) x : ℤ)
    ((((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (X :=
                    ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
                    (ModuleCat.ofHom (πs C o))) :
                (a : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)) →
                  (↑(ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ)) : Type u)) ∘
              eval (π C fun (x : I) ↦ ord I x < o))
            l :
          (a : (↑C : Type u)) → ℤ)
        x :
      ℤ)
have h : Eq (α := ℤ) ((Products.eval C (↑l : Products I) : (a : (↑C : Type u)) → ℤ) x : ℤ)
  ((eval (π C fun (x : I) ↦ ord I x < o) l : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
      (ProjRestrict C (fun (x : I) ↦ ord I x < o) x) :
    ℤ)
Tactic: dsimp [SumEval]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
x : (↑C : Type u)
⊢ Eq (α := ℤ) ((Products.eval C (↑l : Products I) : (a : (↑C : Type u)) → ℤ) x : ℤ)
    ((eval (π C fun (x : I) ↦ ord I x < o) l : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (ProjRestrict C (fun (x : I) ↦ ord I x < o) x) :
      ℤ)
have h : Eq (α := ℤ)
  ((((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            (Products.eval (π C fun (x : I) ↦ ord I x < o) (↑l : Products I)) :
          LocallyConstant (↑C : Type u) ℤ) :
        (a : (↑C : Type u)) → ℤ)
      x :
    ℤ)
  ((eval (π C fun (x : I) ↦ ord I x < o) l : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
      (ProjRestrict C (fun (x : I) ↦ ord I x < o) x) :
    ℤ)
Tactic: rw [← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
⊢ (↑l : List I) = term I ho :: (↑l.Tail : List I)
have rw : term I ho :: (↑l : List I).tail = term I ho :: (↑l.Tail : List I)
Tactic: rw [← List.cons_head!_tail hl, hlh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
⊢ l =
    Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (term I ho :: (↑l.Tail : List I))
      hlc
have simp_rw : l = Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l : List I) sorry
Tactic: simp_rw [← max_eq_o_cons_tail ho l hl hlh, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
⊢ (↑(↑l : Products I) : List I).head! = term I ho
have rw : ord I (↑(↑l : Products I) : List I).head! = o
Tactic: rw [eq_comm, ← ord_term ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
⊢ ord I (↑(↑l : Products I) : List I).head! = o
have hm : term I ho ∈ (↑(↑l : Products I) : List I)
Tactic: have hm := l.prop.2
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
⊢ ord I (↑(↑l : Products I) : List I).head! = o
have this : ord I (↑(↑l : Products I) : List I).head! < Order.succ o
Tactic: have := Products.prop_of_isGood_of_contained C _ l.prop.1 hsC l.val.val.head!
    (List.head!_mem_self (List.ne_nil_of_mem hm))
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! < Order.succ o
⊢ ord I (↑(↑l : Products I) : List I).head! = o
have this₁ : ord I (↑(↑l : Products I) : List I).head! ≤ o
Tactic: simp only [Order.lt_succ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ ord I (↑(↑l : Products I) : List I).head! = o
have refine : o ≤ ord I (↑(↑l : Products I) : List I).head!
Tactic: refine eq_of_le_of_not_lt this (not_lt.mpr ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!
have simp : term I ho ≤ (↑(↑l : Products I) : List I).head!
Tactic: simp only [ord, Ordinal.typein_le_typein, not_lt]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ o ≤ ord I (↑(↑l : Products I) : List I).head!
have h : ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!
Tactic: have h : ord I (term I ho) ≤ ord I l.val.val.head! := by
    simp only [ord, Ordinal.typein_le_typein, not_lt]
    exact Products.rel_head!_of_mem hm
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
h : ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!
⊢ o ≤ ord I (↑(↑l : Products I) : List I).head!
have rwa : ∀ (h : o ≤ ord I (↑(↑l : Products I) : List I).head!), o ≤ ord I (↑(↑l : Products I) : List I).head!
Tactic: rwa [ord_term_aux] at h
Cleared hypotheses: h