awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
x : (↑C : Type u)
⊢ Eq (α := ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ) (ProjRestrict C J) x :
      ℤ)
    ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
have h₁ : Eq (α := ℤ) ((eval (π C J) l : (a : (↑(π C J) : Type u)) → ℤ) (Set.MapsTo.restrict (Proj J) C (π C J) sorry x) : ℤ)
  ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
Tactic: dsimp [ProjRestrict]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
x : (↑C : Type u)
⊢ Eq (α := ℤ) ((eval (π C J) l : (a : (↑(π C J) : Type u)) → ℤ) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) : ℤ)
    ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
have h₁ : Eq (α := ℤ) (if ∀ i ∈ (↑l : List I), (↑(Set.MapsTo.restrict (Proj J) C (π C J) sorry x) : I → Bool) i = true then 1 else 0)
  (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
Tactic: rw [Products.eval_eq, Products.eval_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
⊢ Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
have h₁ : ∀ (x : (↑(π (π C K) J) : Type u)),
  Eq (α := ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) sorry) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
        x :
      ℤ)
    ((eval (π (π C K) J) l : (a : (↑(π (π C K) J) : Type u)) → ℤ) x : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
⊢ Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (ProjRestricts C (J := J) (K := K) hJK))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
have this : Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
  (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
    (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) sorry) : (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
  (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
Tactic: have : l.eval (π C J) ∘ Homeomorph.setCongr (proj_eq_of_subset C J K hJK) =
      l.eval (π (π C K) J) := by
    ext; simp [Homeomorph.setCongr, Products.eval_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this :
  Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
⊢ Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (ProjRestricts C (J := J) (K := K) hJK))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
have rw : Eq (α := (↑(π C K) : Type u) → ℤ)
  (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
    (Function.comp (β := (↑(π (π C K) J) : Type u))
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) sorry) : (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
      (ProjRestrict (π C K) J)))
  (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
Tactic: rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this :
  Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
rw :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (Function.comp (β := (↑(π (π C K) J) : Type u))
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
        (ProjRestrict (π C K) J)))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
⊢ Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (ProjRestricts C (J := J) (K := K) hJK))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
have rw₁ : Eq (α := (↑(π C K) : Type u) → ℤ)
  (Function.comp (β := (↑(π (π C K) J) : Type u))
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) sorry) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (ProjRestrict (π C K) J))
  (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
Tactic: rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this :
  Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
rw :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (Function.comp (β := (↑(π (π C K) J) : Type u))
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
        (ProjRestrict (π C K) J)))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
rw₁ :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π (π C K) J) : Type u))
      (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
      (ProjRestrict (π C K) J))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
⊢ Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (ProjRestricts C (J := J) (K := K) hJK))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
have rw₂ : Eq (α := (↑(π C K) : Type u) → ℤ)
  (Function.comp (β := (↑(π (π C K) J) : Type u)) (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
    (ProjRestrict (π C K) J))
  (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
Tactic: rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
inst_2 : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this :
  Eq (α := (↑(π (π C K) J) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
        (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
    (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
rw :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (Function.comp (β := (↑(π (π C K) J) : Type u))
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
        (ProjRestrict (π C K) J)))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
rw₁ :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π (π C K) J) : Type u))
      (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
        (⇑(Homeomorph.setCongr (s := π (π C K) J) (t := π C J) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u)))
      (ProjRestrict (π C K) J))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
rw₂ :
  Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π (π C K) J) : Type u)) (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
      (ProjRestrict (π C K) J))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
⊢ Eq (α := (↑(π C K) : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ)
      (ProjRestricts C (J := J) (K := K) hJK))
    (⇑(eval (π C K) l) : (a : (↑(π C K) : Type u)) → ℤ)
have rw₃ : Eq (α := (↑(π C K) : Type u) → ℤ)
  (Function.comp (β := (↑(π (π C K) J) : Type u)) (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
    (ProjRestrict (π C K) J))
  (Function.comp (β := (↑(π (π C K) J) : Type u)) (⇑(eval (π (π C K) J) l) : (a : (↑(π (π C K) J) : Type u)) → ℤ)
    (ProjRestrict (π C K) J))
Tactic: rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
⊢ J i
have by_contra : ∀ (h' : ¬J i), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
⊢ False
have apply : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C J) : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (eval (π C J)) {m : Products I | m < l})) (eval (π C J) l)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
this : eval (π C J) l = 0
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C J) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C J)) {m : Products I | m < l})) (eval (π C J) l)
have rw : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C J) : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (eval (π C J)) {m : Products I | m < l})) 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C J) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C J)) {m : Products I | m < l})) (eval (π C J) l)
have suffices : eval (π C J) l = 0
Tactic: suffices eval (π C J) l = 0 by
    rw [this]
    exact Submodule.zero_mem _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
⊢ eval (π C J) l = 0
have h₁ : ∀ (w : I → Bool) (left : w ∈ C),
  Eq (α := ℤ)
    ((eval (π C J) l : (a : (↑(π C J) : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) sorry) :
      ℤ)
    ((0 : (a : (↑(π C J) : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) sorry) : ℤ)
Tactic: ext ⟨_, _, _, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
inst_1 : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
w : I → Bool
left : w ∈ C
⊢ Eq (α := ℤ)
    ((eval (π C J) l : (a : (↑(π C J) : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) ⋯) :
      ℤ)
    ((0 : (a : (↑(π C J) : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) ⋯) : ℤ)
have rw : ∀ (h : ∀ i ∈ (↑l : List I), (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) sorry) : I → Bool) i = true),
  False
Tactic: rw [eval_eq, if_neg fun h ↦ ?_, LocallyConstant.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) ↔
    LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
      (span ℤ (Set.range (ι := Products I) (Products.eval C)))
have refine : ∀
  (h :
    LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
      (span ℤ (Set.range (ι := Products I) (Products.eval C)))),
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) (span ℤ (Set.range (ι := Products I) (Products.eval C)))
    (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)))
Tactic: refine ⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans h ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) (span ℤ (Set.range (ι := Products I) (Products.eval C)))
    (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)))
have rw : Set.range (ι := Products I) (Products.eval C) ⊆
  (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
    Set (LocallyConstant (↑C : Type u) ℤ))
Tactic: rw [span_le]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
⊢ Products.eval C l ∈
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))
have suffices : L l
Tactic: suffices L l by assumption
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
⊢ L l
have ind : ∀ (x : Products I), (∀ y < x, L y) → L x
Tactic: apply IsWellFounded.induction (· < · : Products I → Products I → Prop)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
⊢ L l
have pos : ∀ (hl : Products.isGood C l), L l
Tactic: by_cases hl : l.isGood C
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
pos : ∀ (hl : Products.isGood C l), L l
⊢ L l
have neg : ∀ (hl : ¬Products.isGood C l), L l
Tactic: by_cases hl : l.isGood C
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l
have pos : Products.eval C l ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)
Tactic: apply subset_span
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l
have hl₁ : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
Tactic: simp only [Products.isGood, not_not] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
hl :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
this :
  Set.image (α := Products I) (Products.eval C) {m : Products I | m < l} ⊆
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))
⊢ L l
have this₁ : LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l}))
  (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)))
Tactic: rw [← span_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ (span ℤ (Set.range (ι := Products I) (Products.eval C)))
l_1 : Products I
L : Products I → Prop :=
  fun (m : Products I) ↦
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) (Products.eval C m)
l : Products I
h : ∀ y < l, L y
hl :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < l})) (Products.eval C l)
⊢ L l
have neg : Set.image (α := Products I) (Products.eval C) {m : Products I | m < l} ⊆
  (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
    Set (LocallyConstant (↑C : Type u) ℤ))
Tactic: suffices Products.eval C '' {m | m < l} ⊆ span ℤ (Set.range (GoodProducts.eval C)) by
      rw [← span_le] at this
      exact this hl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
i : I
⊢ ord I i = o ↔ term I ho = i
have refine_1 : ∀ (h : ord I i = o), term I ho = i
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
i : I
refine_1 : ∀ (h : ord I i = o), term I ho = i
⊢ ord I i = o ↔ term I ho = i
have refine_2 : ∀ (h : term I ho = i), ord I i = o
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i
have refine_1 : ∀ (ho : ord I i < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2), term I ho = i
Tactic: subst h
Cleared hypotheses: o, ho, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o
have refine_2 : ord I (term I ho) = o
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
⊢ ord I i < o
have by_contra : ∀ (h' : ¬ord I i < o), False
Tactic: by_contra h'