awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
f : LocallyConstant (↑C : Type u) ℤ
hf :
  Eq (α := (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
C₀C : (↑(C0 C ho) : Type u) → (↑C : Type u) :=
  fun (x : (↑(C0 C ho) : Type u)) ↦ Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯
h₀ : Continuous C₀C
C₁C : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u) → (↑C : Type u) :=
  fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
hx₁' :
  (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) ∈
    π (C1 C ho) fun (x : I) ↦ ord I x < o
⊢ Eq (α := ℤ)
    ((f : (a : (↑C : Type u)) → ℤ)
        (({
                toFun := fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
                  Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯,
                continuous_toFun := h₁ : C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) } :
              (a : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) → (↑C : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
              (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) :
                I → Bool)
              hx₁') :
          (↑C : Type u)) :
      ℤ)
    ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx) : ℤ)
have refine_3 : ({
        toFun := fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
          Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) sorry,
        continuous_toFun := h₁ : C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) } :
      (a : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) → (↑C : Type u))
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
      (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool)
      hx₁') =
  Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx
Tactic: congr
-- 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 : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
f : LocallyConstant (↑C : Type u) ℤ
hf :
  Eq (α := (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
C₀C : (↑(C0 C ho) : Type u) → (↑C : Type u) :=
  fun (x : (↑(C0 C ho) : Type u)) ↦ Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯
h₀ : Continuous C₀C
C₁C : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u) → (↑C : Type u) :=
  fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
hx₁' :
  (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) ∈
    π (C1 C ho) fun (x : I) ↦ ord I x < o
⊢ ({
          toFun := fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
            Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯,
          continuous_toFun := h₁ : C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) } :
        (a : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) → (↑C : Type u))
      (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
        (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool)
        hx₁') =
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx
have refine_3 : SwapTrue o
    (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) =
  x
Tactic: simp only [ContinuousMap.coe_mk, Subtype.mk.injEq]
-- 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}
⊢ Mono (X := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) (ModuleCat.ofHom (πs C o))
have rw : Function.Injective (α := (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u))
  (β := (↑(ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ)) : Type u))
  (⇑(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))
Tactic: rw [ModuleCat.mono_iff_injective]
-- 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 : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat ℤ) (ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
      (ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)))
    (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho)) 0
have hf : ∀ (x : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)),
  Eq (α := (↑(ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)) : Type u))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho)) :
          (a : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)) →
            (↑(ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)) : Type u))
        x :
      (↑(ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) : Type u)) →
            (↑(ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)) : Type u))
        x :
      (↑(ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ)) : Type u))
Tactic: ext : 2
-- 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
⊢ GoodProducts C = GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho
have h : ∀ (l : Products I),
  Membership.mem (γ := Set (Products I)) (GoodProducts C) l ↔
    l ∈ GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : Products I
⊢ Products.isGood C l ↔
    Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
have h : ∀ (h : Products.isGood C l),
  Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
l : Products I
h :
  ∀ (h : Products.isGood C l),
    Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
⊢ Products.isGood C l ↔
    Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
have h₁ : ∀ (h : Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)),
  Products.isGood C l
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
l : Products I
h : Products.isGood C l
⊢ Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
have pos : ∀ (hh : term I ho ∈ (↑l : List I)),
  Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
Tactic: by_cases hh : term I ho ∈ l.val
-- 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
l : Products I
h : Products.isGood C l
pos :
  ∀ (hh : term I ho ∈ (↑l : List I)),
    Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
⊢ Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
have neg : ∀ (hh : term I ho ∉ (↑l : List I)),
  Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
Tactic: by_cases hh : term I ho ∈ l.val
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
⊢ Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
have neg : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
Tactic: left
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
⊢ False
have neg : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
Tactic: apply h
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
have h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i < Order.succ o
Tactic: have h' := Products.prop_of_isGood_of_contained C _ h hsC
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i < Order.succ o
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
have h'₁ : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
Tactic: simp only [Order.lt_succ_iff] at h'
Cleared hypotheses: h'
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
a : I
ha : a ∈ (↑l : List I)
⊢ ord I a < o
have refine : ord I a ≠ o
Tactic: refine (h' a ha).lt_of_ne ?_
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
a : I
ha : a ∈ (↑l : List I)
⊢ ord I a ≠ o
have rw : ¬term I ho = a
Tactic: rw [ne_eq, ord_term ho a]
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
have hh' : ∀ a ∈ (↑l : List I), ord I a < o
Tactic: have hh' : ∀ a ∈ l.val, ord I a < o := by
        intro a ha
        refine (h' a ha).lt_of_ne ?_
        rw [ne_eq, ord_term ho a]
        rintro rfl
        contradiction
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
hh' : ∀ a ∈ (↑l : List I), ord I a < o
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
have neg : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (Submodule.span ℤ
    ((⇑(πs C o) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
      Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
  (Products.eval C l)
Tactic: rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
        Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]
-- 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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ (↑l : List I)
he :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval (π C fun (x : I) ↦ ord I x < o) l)
h' : ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o
hh' : ∀ a ∈ (↑l : List I), ord I a < o
neg :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ
      ((⇑(πs C o) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
        Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (Products.eval C l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
have neg₁ : Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (Submodule.span ℤ
    ((⇑(πs C o) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
      Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
  ((π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) :
    LocallyConstant (↑C : Type u) ℤ)
Tactic: rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
        Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]
-- 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
l : Products I
h : Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
⊢ Products.isGood C l
have hh : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
Tactic: refine h.elim (fun hh ↦ ?_) And.left
-- 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
l : Products I
h : Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)
hh : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ Products.isGood C l
have this : Products.isGood (π C fun (x : I) ↦ ord I x < Order.succ o) l
Tactic: have := Products.isGood_mono C (Order.lt_succ o).le hh
-- 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
⊢ Function.Injective (α := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
    (sum_to C ho)
have refine : ∀ (x : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) (x : (↑(MaxProducts C ho) : Type u)) (a : Products I)
  (ha : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) a) (b : Products I)
  (hb : b ∈ MaxProducts C ho) (hab : a = b), False
Tactic: refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
    (fun ⟨a,ha⟩ ⟨b,hb⟩ ↦ (fun (hab : a = b) ↦ ?_))
-- 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
x : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
x_1 : (↑(MaxProducts C ho) : Type u)
a : Products I
ha : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) a
b : Products I
hb : b ∈ MaxProducts C ho
hab : a = b
⊢ False
have hb₁ : a ∈ MaxProducts C ho
Tactic: rw [← hab] at hb
Cleared hypotheses: hb, hab
-- 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
x : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
x_1 : (↑(MaxProducts C ho) : Type u)
a : Products I
ha : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) a
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
⊢ False
have ha' : ord I (term I ho) < o
Tactic: have ha' := Products.prop_of_isGood C _ ha (term I ho) hb.2