awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
x : { l : Products I // Products.isGood ∅ l }
l : Products I
hl : Products.isGood ∅ l
rw :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑∅ : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval ∅) {m : Products I | m < l})) 0
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑∅ : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval ∅) {m : Products I | m < l})) (Products.eval ∅ l)

Tactic:
rw [subsingleton_iff.mp inferInstance (Products.eval ∅ l) 0]

Premises used: subsingleton_iff, Profinite.NobelingProof.Products.eval, inferInstance, Iff.mp, EmptyCollection.emptyCollection, OfNat.ofNat
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
x : { l : Products I // Products.isGood ∅ l }
l : Products I
hl : Products.isGood ∅ l
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑∅ : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval ∅) {m : Products I | m < l})) 0

Tactic:
Submodule.zero_mem _

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
x : { l : Products I // Products.isGood ∅ l }
l : Products I
hl : Products.isGood ∅ l
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑∅ : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval ∅) {m : Products I | m < l})) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
⊢ LinearIndependent.{u_1, 0, u_1} (ι := { l : Products I // Products.isGood ∅ l }) ℤ (eval ∅)

Tactic:
linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) []

Tactic:
simp only [List.isChain_nil]

Premises used: List.isChain_nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
h :
  ∀ (m : List I) (hm : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) m),
    Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
        (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm) ↔
      Membership.mem (γ := Set (Products I)) ∅
        (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)
⊢ Eq.{u_1 + 1} (α := Set (Products I)) {m : Products I | m < nil} ∅

Tactic:
ext ⟨m, hm⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
m : List I
hm : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) m
tauto :
  Membership.mem (γ := Set (Products I)) ∅
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm) →
    Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)
⊢ Membership.mem (γ := Set (Products I)) ∅
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm) →
    Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)

Tactic:
tauto
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
m : List I
hm : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) m
h :
  ∀
    (h :
      Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
        (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)),
    Membership.mem (γ := Set (Products I)) ∅
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)
⊢ Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm) ↔
    Membership.mem (γ := Set (Products I)) ∅
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)

Tactic:
refine ⟨fun h ↦ ?_, by tauto⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
m : List I
hm : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) m
h :
  Membership.mem (γ := Set (Products I)) {m : Products I | m < nil}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)
⊢ Membership.mem (γ := Set (Products I)) ∅
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) m hm)

Tactic:
simp only [Set.mem_setOf_eq, lt_iff_lex_lt, nil, List.not_lex_nil] at h

Premises used: Set.mem_setOf_eq, Profinite.NobelingProof.Products.lt_iff_lex_lt, List.not_lex_nil, Profinite.NobelingProof.Products.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : Nonempty α
⊢ Nontrivial.{u_1} (LocallyConstant α ℤ)

Tactic:
⟨0, 1, ne_of_apply_ne DFunLike.coe <| (Function.const_injective (β := ℤ)).ne zero_ne_one⟩

Premises used: Function.Injective.ne, zero_ne_one, Nontrivial.mk, Function.const_injective, ne_of_apply_ne, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
h :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval {fun (x : I) ↦ false}) {m : Products I | m < nil}))
    (eval {fun (x : I) ↦ false} nil)
⊢ False

Tactic:
simp [Products.eval, Products.nil] at h

Premises used: Profinite.NobelingProof.Products.eval, Profinite.NobelingProof.Products.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
rw :
  LE.le (α := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤
    (ℤ ∙ eval {fun (x : I) ↦ false} nil)
⊢ Eq (α := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval {fun (x : I) ↦ false}) {nil})) ⊤

Tactic:
rw [Set.image_singleton, eq_top_iff]

Premises used: eq_top_iff, Set.image_singleton
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
_ :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
      (ℤ ∙ eval {fun (x : I) ↦ false} nil) f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
      (ℤ ∙ eval {fun (x : I) ↦ false} nil) f

Tactic:
_
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
rw :
  ∃ (a : ℤ),
    HSMul.hSMul (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) a (eval {fun (x : I) ↦ false} nil) = f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
    (ℤ ∙ eval {fun (x : I) ↦ false} nil) f

Tactic:
rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
⊢ ∃ (a : ℤ),
    HSMul.hSMul (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) a (eval {fun (x : I) ↦ false} nil) = f

Tactic:
⟨f default, ?_⟩

Premises used: Inhabited.default, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
refine :
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)
      ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default : ℤ) (eval {fun (x : I) ↦ false} nil) =
    f
⊢ ∃ (a : ℤ),
    HSMul.hSMul (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) a (eval {fun (x : I) ↦ false} nil) = f

Tactic:
refine ⟨f default, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
simp :
  (↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
      LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) =
    f
⊢ HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)
      ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default : ℤ) (eval {fun (x : I) ↦ false} nil) =
    f

Tactic:
simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]

Premises used: zsmul_eq_mul, Profinite.NobelingProof.Products.eval, List.map, List.prod_nil, mul_one, Profinite.NobelingProof.Products.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
h :
  ∀ (x : (↑{fun (x : I) ↦ false} : Type u_1)),
    Eq (α := ℤ)
      (((↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
              LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) :
            (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ)
          x :
        ℤ)
      ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) x : ℤ)
⊢ (↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
      LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) =
    f

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
x : (↑{fun (x : I) ↦ false} : Type u_1)
⊢ x = default

Tactic:
simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]

Premises used: Set.default_coe_singleton, eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
x : (↑{fun (x : I) ↦ false} : Type u_1)
h :
  Eq (α := ℤ)
    (((↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
            LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) :
          (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ)
        default :
      ℤ)
    ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default : ℤ)
⊢ Eq (α := ℤ)
    (((↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
            LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) :
          (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ)
        x :
      ℤ)
    ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) x : ℤ)

Tactic:
obtain rfl : x = default := by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]

Premises used: Inhabited.default, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
f : LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ f
⊢ Eq (α := ℤ)
    (((↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
            LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) :
          (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ)
        default :
      ℤ)
    ((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default : ℤ)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
a :
  (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l)
          (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl) hll) :
      Products I) =
    (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l) Products.nil ⋯) : Products I)
⊢ Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l)
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl) hll =
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l) Products.nil ⋯

Tactic:
ext
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
a :
  (↑(↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l)
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl) hll) :
          Products I) :
      List I) =
    (↑(↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l) Products.nil ⋯) :
          Products I) :
      List I)
⊢ (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l)
          (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl) hll) :
      Products I) =
    (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l) Products.nil ⋯) : Products I)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
a : ¬List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
⊢ (↑(↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l)
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl) hll) :
          Products I) :
      List I) =
    (↑(↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood {fun (x : I) ↦ false} l) Products.nil ⋯) :
          Products I) :
      List I)

Tactic:
apply (List.lex_nil_or_eq_nil l (r := (· < ·))).resolve_left

Premises used: Or.resolve_left, List.lex_nil_or_eq_nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
a :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false})
        {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
⊢ False

Tactic:
apply hll
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
⊢ Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}

Tactic:
simpa only [Products.nil, Products.lt_iff_lex_lt, Set.singleton_subset_iff, Set.mem_setOf_eq]

Premises used: Set.singleton_subset_iff, Set.mem_setOf_eq, Profinite.NobelingProof.Products.lt_iff_lex_lt, Profinite.NobelingProof.Products.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
⊢ Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}

Tactic:
have he : {Products.nil} ⊆ {m | m < ⟨l,hl⟩} := by
      simpa only [Products.nil, Products.lt_iff_lex_lt, Set.singleton_subset_iff, Set.mem_setOf_eq]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
a :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false}) {Products.nil}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false})
        {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))

Tactic:
grw [← he]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
a :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ)) ⊤
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false}) {Products.nil}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))

Tactic:
rw [Products.span_nil_eq_top]

Premises used: Profinite.NobelingProof.Products.span_nil_eq_top
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ)) ⊤
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))

Tactic:
Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ)) ⊤
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
α : Type u_1
inst_1 : TopologicalSpace α
⊢ IsAddTorsionFree.{u_1} (LocallyConstant α ℤ)

Tactic:
LocallyConstant.coe_injective.isAddTorsionFree LocallyConstant.coeFnAddMonoidHom

Premises used: LocallyConstant.coeFnAddMonoidHom, LocallyConstant.coe_injective, Function.Injective.isAddTorsionFree
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u_1
inst : LinearOrder I
⊢ Ne (α := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) (eval {fun (x : I) ↦ false} default) 0

Tactic:
simp [eval, Products.eval, Products.nil, default]

Premises used: Inhabited.default, Profinite.NobelingProof.Products.eval, Profinite.NobelingProof.GoodProducts.eval, Profinite.NobelingProof.Products.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective (β := (↑(smaller C o) : Type u)) fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
    Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
      ⋯

Tactic:
⟨fun a b hab ↦ ?_, fun ⟨a, b, hb⟩ ↦ ?_⟩

Premises used: Profinite.NobelingProof.πs, Exists, Subtype.mk, And.intro, Function.Bijective, Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun._proof_1, _private.0.Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective.match_1, Subtype.val, Eq, DFunLike.coe