awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ 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:
C1_projOrd C hsC ho hx₁

Premises used: Profinite.NobelingProof.Proj, Profinite.NobelingProof.C1_projOrd, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ 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:
exact C1_projOrd C hsC ho hx₁

Premises used: Profinite.NobelingProof.C1_projOrd
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
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))
⊢ Mono (X := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) (ModuleCat.ofHom (πs C o))

Tactic:
rw [ModuleCat.mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ 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:
injective_πs _ _

Premises used: Profinite.NobelingProof.injective_πs
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ 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:
exact injective_πs _ _

Premises used: Profinite.NobelingProof.injective_πs
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
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))
⊢ 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

Tactic:
ext : 2
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
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:
apply CC_comp_zero

Premises used: Profinite.NobelingProof.CC_comp_zero
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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 :
  ∀ (l : Products I),
    Membership.mem (γ := Set (Products I)) (GoodProducts C) l ↔
      l ∈ GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho
⊢ GoodProducts C = GoodProducts (π C fun (x : I) ↦ ord I x < o) ∪ MaxProducts C ho

Tactic:
ext l
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)

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

Premises used: Iff.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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)
⊢ 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

Premises used: Profinite.NobelingProof.term, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)

Tactic:
Or.inr ⟨h, hh⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)

Tactic:
exact Or.inr ⟨h, hh⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
neg : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ Products.isGood (π C fun (x : I) ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ (↑l : List I)

Tactic:
left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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)
⊢ False

Tactic:
apply h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
⊢ ∀ (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
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ ∀ (i : I) (hi : i ∈ (↑l : List I)), ord I i ≤ o

Tactic:
simp only [Order.lt_succ_iff] at h'

Premises used: Order.lt_succ_iff
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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

Tactic:
(h' a ha).lt_of_ne ?_

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
refine : ord I a ≠ o
⊢ ord I a < o

Tactic:
refine (h' a ha).lt_of_ne ?_

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
rw : ¬term I ho = a
⊢ ord I a ≠ o

Tactic:
rw [ne_eq, ord_term ho a]

Premises used: Profinite.NobelingProof.ord_term, ne_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
ha : term I ho ∈ (↑l : List I)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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 ∈ (↑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
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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) ℤ)
neg₂ neg₃ neg₄ neg₅ :
  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)

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

Premises used: Profinite.NobelingProof.Products.eval_πs, Submodule.apply_mem_span_image_iff_mem_span, Profinite.NobelingProof.injective_πs, Profinite.NobelingProof.Products.eval_πs_image
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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

Tactic:
h.elim (fun hh ↦ ?_) And.left

Premises used: And.left, Or.elim
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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 fun (x : I) ↦ ord I x < o) l

Tactic:
refine h.elim (fun hh ↦ ?_) And.left

Premises used: And.left, Or.elim
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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 fun (x : I) ↦ ord I x < Order.succ o) l

Tactic:
have := Products.isGood_mono C (Order.lt_succ o).le hh
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
this : Products.isGood (π C fun (x : I) ↦ ord I x < Order.succ o) l
h₁ h₂ h₃ h₄ : Products.isGood (π C fun (x : I) ↦ ord I x < Order.succ o) l
⊢ Products.isGood C l

Tactic:
rwa [contained_eq_proj C (Order.succ o) hsC]

Premises used: Order.succ, Profinite.NobelingProof.contained_eq_proj