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
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' C ho) : Type u) ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (Products.eval C (↑l : Products I)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
⊢ Membership.mem (γ := Set (Products I)) {m : Products I | m < (↑l : Products I)}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (term I ho :: (↑q : List I)) ⋯)
have h₂ : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (↑(↑l : Products I) : List I)
Tactic: simp only [Products.lt_iff_lex_lt, Set.mem_setOf_eq]
-- 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
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' C ho) : Type u) ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (Products.eval C (↑l : Products I)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (↑(↑l : Products I) : List I)
have h₂ : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (term I ho :: (↑(↑l : Products I).Tail : List I))
Tactic: rw [max_eq_o_cons_tail C hsC ho 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ m = n
have apply : (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
  (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
Tactic: apply Subtype.ext ∘ Subtype.ext
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
have h₂ : (↑(MaxToGood C hC hsC ho h₁ m) : Products I) = (↑(MaxToGood C hC hsC ho h₁ n) : Products I)
Tactic: rw [Subtype.ext_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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : (↑m : Products I).Tail = (↑n : Products I).Tail
⊢ (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
have rw : term I ho :: (↑(↑m : Products I).Tail : List I) =
  (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
Tactic: rw [max_eq_o_cons_tail C hsC ho m, max_eq_o_cons_tail C hsC ho n, 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : (↑m : Products I).Tail = (↑n : Products I).Tail
rw :
  term I ho :: (↑(↑m : Products I).Tail : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
⊢ (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
have rw₁ : term I ho :: (↑(↑m : Products I).Tail : List I) = term I ho :: (↑(↑n : Products I).Tail : List I)
Tactic: rw [max_eq_o_cons_tail C hsC ho m, max_eq_o_cons_tail C hsC ho n, 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : (↑m : Products I).Tail = (↑n : Products I).Tail
rw :
  term I ho :: (↑(↑m : Products I).Tail : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
rw₁ : term I ho :: (↑(↑m : Products I).Tail : List I) = term I ho :: (↑(↑n : Products I).Tail : List I)
⊢ (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
have rw₂ : term I ho :: (↑(↑n : Products I).Tail : List I) = term I ho :: (↑(↑n : Products I).Tail : List I)
Tactic: rw [max_eq_o_cons_tail C hsC ho m, max_eq_o_cons_tail C hsC ho n, 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
⊢ LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho)) →
    LinearIndependent (ι := (↑(MaxProducts C ho) : Type u)) ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
        (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
have rw : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho)) →
  LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
    Products.eval (C' C ho) (↑l : Products I).Tail
Tactic: rw [max_eq_eval_unapply C hsC ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
⊢ LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
    Products.eval (C' C ho) (↑l : Products I).Tail
have hf : Function.Injective f
Tactic: have hf : f.Injective := maxToGood_injective C hC hsC ho 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
⊢ LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
    Products.eval (C' C ho) (↑l : Products I).Tail
have hh : (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f
Tactic: have hh : (fun l ↦ Products.eval (C' C ho) l.val.Tail) = eval (C' C ho) ∘ f := rfl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
    Products.eval (C' C ho) (↑l : Products I).Tail
have rw : LinearIndependent ℤ (eval (C' C ho) ∘ f)
Tactic: rw [hh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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})) (Products.eval ∅ l)
have rw : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑∅ : Type u) ℤ))
  (Submodule.span ℤ (Set.image (α := Products I) (Products.eval ∅) {m : Products I | m < l})) 0
Tactic: rw [subsingleton_iff.mp inferInstance (Products.eval ∅ l) 0]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u_1
inst : LinearOrder I
⊢ Eq.{u_1 + 1} (α := Set (Products I)) {m : Products I | m < nil} ∅
have 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)
Tactic: ext ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u_1
inst : LinearOrder I
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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, by tauto⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u_1
inst : LinearOrder I
⊢ Eq (α := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval {fun (x : I) ↦ false}) {nil})) ⊤
have rw : LE.le (α := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ)) ⊤ (ℤ ∙ eval {fun (x : I) ↦ false} nil)
Tactic: rw [Set.image_singleton, eq_top_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ))
    (ℤ ∙ eval {fun (x : I) ↦ false} nil) f
have rw : ∃ (a : ℤ),
  HSMul.hSMul (β := LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) a (eval {fun (x : I) ↦ false} nil) = f
Tactic: rw [Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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
have 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
Tactic: refine ⟨f default, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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
⊢ 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
have simp : (↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
    LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) =
  f
Tactic: simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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
⊢ (↑((f : (a : (↑{fun (x : I) ↦ false} : Type u_1)) → ℤ) default) :
      LocallyConstant (↑{fun (x : I) ↦ false} : Type u_1) ℤ) =
    f
have 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 : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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)
⊢ 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 : ℤ)
have 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 : ℤ)
Tactic: obtain rfl : x = default := by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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)
⊢ 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 ⋯
have 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 sorry) : Products I)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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)
⊢ (↑(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)
have 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 sorry) : Products I) :
    List I)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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)
⊢ (↑(↑(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)
have a : ¬List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
Tactic: apply (List.lex_nil_or_eq_nil l (r := (· < ·))).resolve_left