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}
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)

Tactic:
Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
    (fun ⟨a,ha⟩ ⟨b,hb⟩ ↦ (fun (hab : a = b) ↦ ?_))

Premises used: Profinite.NobelingProof.GoodProducts.sum_to, Subtype.val_injective, Ne, _private.0.Profinite.NobelingProof.GoodProducts.injective_sum_to.match_2, Subtype.mk, Subtype.val, Function.Injective.sumElim, _private.0.Profinite.NobelingProof.GoodProducts.injective_sum_to.match_1
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
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
⊢ Function.Injective (α := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
    (sum_to C ho)

Tactic:
refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
    (fun ⟨a,ha⟩ ⟨b,hb⟩ ↦ (fun (hab : a = b) ↦ ?_))
-- 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}
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
⊢ a ∈ MaxProducts C ho

Tactic:
rw [← hab] at hb
-- 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}
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
hb₁ : a ∈ MaxProducts C ho
⊢ a = b

Tactic:
rw [← hab] at hb
-- 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}
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
⊢ ord I (term I ho) < o

Tactic:
have ha' := Products.prop_of_isGood C _ ha (term I ho) hb.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}
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
ha' : ord I (term I ho) < o
⊢ False

Tactic:
simp only [ord_term_aux, lt_self_iff_false] at ha'

Premises used: Profinite.NobelingProof.ord_term_aux, lt_self_iff_false
-- 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}
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) =
    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 _ _
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
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))
⊢ 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

Tactic:
simp_all
-- 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_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
rw₁ 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
⊢ Set.range (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho) : Type u))
      (sum_to C ho) =
    GoodProducts C

Tactic:
rw [sum_to_range C ho, union_succ C hsC ho]

Premises used: Profinite.NobelingProof.GoodProducts.sum_to_range, Profinite.NobelingProof.GoodProducts.union_succ
-- 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 :
  ∀ (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 :
        ℤ)
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 :
        ℤ)
⊢ 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)

Tactic:
ext ⟨_, _⟩
-- 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
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:
rfl
-- 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
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:
rfl
-- 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
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)
⊢ 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)

Tactic:
rw [← linearIndependent_equiv (sum_equiv C hsC ho), SumEval,
    ← sum_equiv_comp_eval_eq_elim C hsC ho]

Premises used: Profinite.NobelingProof.GoodProducts.sum_equiv, linearIndependent_equiv, Profinite.NobelingProof.GoodProducts.SumEval, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_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
⊢ 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:
Iff.rfl

Premises used: Iff.rfl
-- 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
⊢ 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:
exact Iff.rfl

Premises used: Iff.rfl
-- 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
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)))
rw₂ rw₃ :
  Set.range (ι := { l : Products I // Products.isGood C l }) (eval C) =
    Set.range (ι := (↑(GoodProducts C) : Type u)) (eval C)
⊢ 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))

Tactic:
rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
    EquivLike.range_comp (e := sum_equiv C hsC ho)]

Premises used: Equiv.toFun_as_coe, Profinite.NobelingProof.GoodProducts.sum_equiv, EquivLike.range_comp, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
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 :
        ℤ)
⊢ 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)

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}
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)
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) :
      ℤ)
⊢ 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:
dsimp [SumEval]

Premises used: Profinite.NobelingProof.GoodProducts.SumEval
-- 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}
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)
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) :
      ℤ)
⊢ 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:
rw [← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)]

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.prop_of_isGood, Subtype.prop
-- 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}
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 (α := ℤ)
    ((((π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:
simp [eval]

Premises used: Profinite.NobelingProof.GoodProducts.eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
⊢ SwapTrue o x (term I ho) = true

Tactic:
simp only [SwapTrue, ord_term_aux, ite_true]

Premises used: Profinite.NobelingProof.ord_term_aux, ite_true, Profinite.NobelingProof.SwapTrue
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : I → Bool
left : y ∈ C1 C ho
left_1 : Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 C ho
⊢ Proj (fun (x : I) ↦ ord I x < o) y (term I ho) = false

Tactic:
simp only [Proj, ord_term_aux, lt_self_iff_false, ite_false]

Premises used: Profinite.NobelingProof.ord_term_aux, ite_false, Profinite.NobelingProof.Proj, lt_self_iff_false
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
rw : term I ho :: (↑l : List I).tail = term I ho :: (↑l.Tail : List I)
⊢ (↑l : List I) = term I ho :: (↑l.Tail : List I)

Tactic:
rw [← List.cons_head!_tail hl, hlh]

Premises used: List.cons_head!_tail
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ term I ho :: (↑l : List I).tail = term I ho :: (↑l.Tail : List I)

Tactic:
simp [Tail]

Premises used: Profinite.NobelingProof.Products.Tail
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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))
simp_rw : l = Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l : 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

Tactic:
simp_rw [← max_eq_o_cons_tail ho l hl hlh, Subtype.coe_eta]

Premises used: Subtype.coe_eta, Profinite.NobelingProof.Products.max_eq_o_cons_tail
-- 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
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
rw : ord I (↑(↑l : Products I) : List I).head! = o
⊢ (↑(↑l : Products I) : List I).head! = term I ho

Tactic:
rw [eq_comm, ← ord_term ho]

Premises used: Profinite.NobelingProof.ord_term, eq_comm
-- 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
inst_2 : Inhabited I
l : (↑(MaxProducts C ho) : Type u)
⊢ term I ho ∈ (↑(↑l : Products I) : List I)

Tactic:
have hm := l.prop.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}
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! < 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))
-- 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
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

Tactic:
simp only [Order.lt_succ_iff] at this

Premises used: Order.lt_succ_iff