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
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)
h' : ¬ord I i < o
⊢ False
have apply : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (eval C) {m : Products I | m < l})) (eval C 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
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)
h' : ¬ord I i < o
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval C) {m : Products I | m < l})) (eval C l)
have suffices : eval C l = 0
Tactic: suffices eval C l = 0 by simp [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
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
⊢ eval C l = 0
have h₁ : ∀ (x : (↑C : Type u)), Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ) ((0 : (a : (↑C : Type u)) → ℤ) x : ℤ)
Tactic: ext x
-- 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)
h' : ¬ord I i < o
x : (↑C : Type u)
⊢ Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ) ((0 : (a : (↑C : Type u)) → ℤ) x : ℤ)
have h₁ : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) → False
Tactic: simp only [eval_eq, LocallyConstant.coe_zero, Pi.zero_apply, ite_eq_right_iff, one_ne_zero]
-- 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)
h' : ¬ord I i < o
x : (↑C : Type u)
⊢ (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) → False
have h₁ : ∀ (h' : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) ∧ True), ord I i < o
Tactic: contrapose! h'
Cleared hypotheses: h'
-- 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
o : Ordinal.{u}
h : contained C o
⊢ C = π C fun (x : I) ↦ ord I x < o
have this : ∀ (hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → ord I i < o), (π C fun (x : I) ↦ ord I x < o) = C
Tactic: have := proj_prop_eq_self C (ord I · < o)
-- 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
o : Ordinal.{u}
h : contained C o
this : ∀ (hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → ord I i < o), (π C fun (x : I) ↦ ord I x < o) = C
⊢ C = π C fun (x : I) ↦ ord I x < o
have this₁ : ∀ (hh : ∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o), (Proj fun (x : I) ↦ ord I x < o) '' C = C
Tactic: simp only [ne_eq, Bool.not_eq_false, π] 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
o : Ordinal.{u}
x : I → Bool
⊢ (x ∈ π C fun (x : I) ↦ ord I x < o) → ∀ (i : I), x i = true → ord I i < o
have this : ∀ w ∈ C, ∀ (h : Proj (fun (x : I) ↦ ord I x < o) w = x) (i : I), x i = true → ord I i < o
Tactic: ⟨_, _, 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ (↑l : List I), ord I i < o₁
⊢ (πs' C h :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < o₁) l) =
    eval (π C fun (x : I) ↦ ord I x < o₂) l
have rw : Eq (α := (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
  (LocallyConstant.toFun
    ((πs' C h :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < o₁) l)))
  (⇑(eval (π C fun (x : I) ↦ ord I x < o₂) l) : (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
Tactic: rw [← LocallyConstant.coe_inj, ← LocallyConstant.toFun_eq_coe]
-- 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}
hl : ∀ i ∈ (↑l : List I), ord I i < o
⊢ Set.image (α := Products I) (eval C) {m : Products I | m < l} =
    (⇑(πs C o) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
      Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}
have h : ∀ (f : LocallyConstant (↑C : Type u) ℤ),
  f ∈ Set.image (α := Products I) (eval C) {m : Products I | m < l} ↔
    Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
      ((⇑(πs C o) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
        Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l})
      f
Tactic: ext f
-- 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}
hl : ∀ i ∈ (↑l : List I), ord I i < o
f : LocallyConstant (↑C : Type u) ℤ
⊢ f ∈ Set.image (α := Products I) (eval C) {m : Products I | m < l} ↔
    Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
      ((⇑(πs C o) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
        Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l})
      f
have h : (∃ x < l, eval C x = f) ↔
  ∃ a < l,
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o) a) =
      f
Tactic: simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]
-- 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}
hl : ∀ i ∈ (↑l : List I), ord I i < o
f : LocallyConstant (↑C : Type u) ℤ
⊢ (∃ x < l, eval C x = f) ↔
    ∃ a < l,
      (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o) a) =
        f
have h : ∀ (a : Products I),
  a < l ∧ eval C a = f ↔
    a < l ∧
      (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o) a) =
        f
Tactic: apply exists_congr
-- 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}
hl : ∀ i ∈ (↑l : List I), ord I i < o
f : LocallyConstant (↑C : Type u) ℤ
m : Products I
⊢ m < l ∧ eval C m = f ↔
    m < l ∧
      (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o) m) =
        f
have h : m < l →
  (eval C m = f ↔
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o) m) =
      f)
Tactic: apply and_congr_right
-- 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}
hl : ∀ i ∈ (↑l : List I), ord I i < o
f : LocallyConstant (↑C : Type u) ℤ
m : Products I
hm : m < l
⊢ eval C m = f ↔
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o) m) =
      f
have h : eval C m = f ↔ eval C m = f
Tactic: rw [eval_πs C (lt_ord_of_lt hm hl)]
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ (↑l : List I), ord I i < o₁
⊢ Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l} =
    (⇑(πs' C h) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
      Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}
have h₁ : ∀ (f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ),
  f ∈ Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l} ↔
    Membership.mem (γ := Set (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
      ((⇑(πs' C h) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
        Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l})
      f
Tactic: ext f
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ (↑l : List I), ord I i < o₁
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ
⊢ f ∈ Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l} ↔
    Membership.mem (γ := Set (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
      ((⇑(πs' C h) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
        Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l})
      f
have h₁ : (∃ x < l, eval (π C fun (x : I) ↦ ord I x < o₂) x = f) ↔
  ∃ a < l,
    (πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁) a) =
      f
Tactic: simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ (↑l : List I), ord I i < o₁
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ
⊢ (∃ x < l, eval (π C fun (x : I) ↦ ord I x < o₂) x = f) ↔
    ∃ a < l,
      (πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁) a) =
        f
have h₁ : ∀ (a : Products I),
  a < l ∧ eval (π C fun (x : I) ↦ ord I x < o₂) a = f ↔
    a < l ∧
      (πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁) a) =
        f
Tactic: apply exists_congr
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ (↑l : List I), ord I i < o₁
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ
m : Products I
⊢ m < l ∧ eval (π C fun (x : I) ↦ ord I x < o₂) m = f ↔
    m < l ∧
      (πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁) m) =
        f
have h₁ : m < l →
  (eval (π C fun (x : I) ↦ ord I x < o₂) m = f ↔
    (πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁) m) =
      f)
Tactic: apply and_congr_right
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ (↑l : List I), ord I i < o₁
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ
m : Products I
hm : m < l
⊢ eval (π C fun (x : I) ↦ ord I x < o₂) m = f ↔
    (πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁) m) =
      f
have h₁ : eval (π C fun (x : I) ↦ ord I x < o₂) m = f ↔ eval (π C fun (x : I) ↦ ord I x < o₂) m = f
Tactic: rw [eval_πs' C h (lt_ord_of_lt hm hl)]
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun (x : I) ↦ ord I x < o₁) l
hl' :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₂) l)
⊢ False
have apply : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
  (eval (π C fun (x : I) ↦ ord I x < o₁) l)
Tactic: apply hl
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun (x : I) ↦ ord I x < o₁) l
hl' :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₂) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₁) l)
have rwa : ∀
  (hl' :
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
      (span ℤ
        ((⇑(πs' C h) :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
          Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o₂) l)),
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₁) l)
Tactic: rwa [eval_πs_image' C h (prop_of_isGood C _ hl), ← eval_πs' C h (prop_of_isGood C _ hl),
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C h)] at hl'
Cleared hypotheses: hl'
-- 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₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun (x : I) ↦ ord I x < o₁) l
hl' :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₂) l)
rwa :
  ∀
    (hl' :
      Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
        (span ℤ
          ((⇑(πs' C h) :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
            Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
        (eval (π C fun (x : I) ↦ ord I x < o₂) l)),
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
      (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o₁) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₁) l)
have rwa₁ : ∀
  (hl' :
    Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) (γ :=
      Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
      (span ℤ
        ((⇑(πs' C h) :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
          Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁) l) :
        LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)),
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₁) l)
Tactic: rwa [eval_πs_image' C h (prop_of_isGood C _ hl), ← eval_πs' C h (prop_of_isGood C _ hl),
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C h)] at hl'
Cleared hypotheses: hl'
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
⊢ Membership.mem (γ := Set (I → Bool)) {fun (x : I) ↦ false} c
have h : ∀ (x : I), c x = false
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (hypothesis)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have this : C ⊆ {fun (x : I) ↦ false}
Tactic: have : C ⊆ {(fun _ ↦ false)} := fun c hc ↦ by
    ext x; exact Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (hypothesis)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
this : C ⊆ {fun (x : I) ↦ false}
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have this₁ : C = ∅ ∨ C = {fun (x : I) ↦ false}
Tactic: rw [Set.subset_singleton_iff_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun (x : I) ↦ false}
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have inl : C = ∅ → LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun (x : I) ↦ false}
inl : C = ∅ → LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have inr : C = {fun (x : I) ↦ false} → LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
h_2 : C = ∅
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have inl : IsClosed.{u} (X := I → Bool) ∅ →
  ∀ (hsC : contained.{u} (I := I) ∅ 0),
    LinearIndependent.{u, 0, u} (ι := { l : Products I // Products.isGood ∅ l }) ℤ (eval ∅)
Tactic: subst C
Cleared hypotheses: C, h_1, hsC, h_2
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_1 : IsClosed C
hsC : contained C 0
h_2 : C = {fun (x : I) ↦ false}
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have inr : IsClosed (X := I → Bool) {fun (x : I) ↦ false} →
  ∀ (hsC : contained (I := I) {fun (x : I) ↦ false} 0),
    LinearIndependent (ι := { l : Products I // Products.isGood {fun (x : I) ↦ false} l }) ℤ
      (eval {fun (x : I) ↦ false})
Tactic: subst C
Cleared hypotheses: C, h_1, hsC, h_2
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have rw : LinearIndepOn.{u, 0, u} (ι := LocallyConstant (↑C : Type u) ℤ) ℤ id
  (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u}))
Tactic: rw [linearIndependent_iff_union_smaller C ho hsC, linearIndependent_subtype_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ : Ordinal.{u}
⊢ P I μ
have refine : ∀ (o : Ordinal.{u}) (h : P I o) (ho : o + 1 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2) (C : Set (I → Bool))
  (hC : IsClosed C) (hsC : contained C (o + 1)),
  LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
Tactic: refine Ordinal.limitRecOn μ P0 (fun o h ho C hC hsC ↦ ?_)
      (fun o ho h ↦ (GoodProducts.Plimit o ho (fun o' ho' ↦ (h o' ho'))))