awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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 = true → ord I i < o), (Proj fun (x : I) ↦ ord I x < o) '' C = C
⊢ C = π C fun (x : I) ↦ ord I x < o

Tactic:
(this (fun i x hx ↦ h x hx i)).symm

Premises used: Profinite.NobelingProof.π, Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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 = true → ord I i < o), (Proj fun (x : I) ↦ ord I x < o) '' C = C
⊢ C = π C fun (x : I) ↦ ord I x < o

Tactic:
exact (this (fun i x hx ↦ h x hx i)).symm

Premises used: Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
⊢ IsClosed (π C fun (x : I) ↦ ord I x < o)

Tactic:
(continuous_proj (ord I · < o)).isClosedMap C hC

Premises used: Profinite.NobelingProof.π, Continuous.isClosedMap, Profinite.NobelingProof.ord, LT.lt, Profinite.NobelingProof.continuous_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
x : I → Bool
this : ∀ w ∈ C, ∀ (h : Proj (fun (x : I) ↦ ord I x < o) w = x) (i : I), x i = true → ord I i < o
⊢ (x ∈ π C fun (x : I) ↦ ord I x < o) → ∀ (i : I), x i = true → ord I i < o

Tactic:
⟨_, _, h⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
x w : I → Bool
left : w ∈ C
h : Proj (fun (x : I) ↦ ord I x < o) w = x
j : I
hj : x j = true
⊢ ord I j < o

Tactic:
aesop (add simp Proj)

Premises used: Profinite.NobelingProof.Proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
⊢ Eq (α := (a : (↑C : Type u)) → ℤ)
    (⇑((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            f :
          LocallyConstant (↑C : Type u) ℤ) :
      (a : (↑C : Type u)) → ℤ)
    (Function.comp (β := (↑(π C fun (x : I) ↦ ord I x < o) : Type u))
      (⇑f : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ) (ProjRestrict C fun (x : I) ↦ ord I x < o))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Injective (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (β :=
    LocallyConstant (↑C : Type u) ℤ)
    (⇑(πs C o) : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)

Tactic:
LocallyConstant.comap_injective ⟨_, (continuous_projRestrict _ _)⟩
    (Set.surjective_mapsTo_image_restrict _ _)

Premises used: LocallyConstant.comap, ContinuousMap.mk, Set.surjective_mapsTo_image_restrict, Profinite.NobelingProof.continuous_projRestrict, LocallyConstant.comap_injective
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
f : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ
⊢ Eq (α := (↑(π 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) ℤ)
        f))
    (f.toFun ∘ ProjRestricts C (J := fun (x : I) ↦ ord I x < o₁) (K := fun (x : I) ↦ ord I x < o₂) ⋯)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
⊢ Function.Injective (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) (β :=
    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) ℤ)

Tactic:
LocallyConstant.comap_injective ⟨_, (continuous_projRestricts _ _)⟩
    (surjective_projRestricts _ fun _ hi ↦ lt_of_lt_of_le hi h)

Premises used: LocallyConstant.comap, ContinuousMap.mk, Profinite.NobelingProof.continuous_projRestricts, LocallyConstant.comap_injective, lt_of_lt_of_le, Profinite.NobelingProof.surjective_projRestricts
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
l m : Products I
o : Ordinal.{u}
h₁ : m < l
h₂ : ∀ i ∈ (↑l : List I), ord I i < o
⊢ ∀ i ∈ (↑m : List I), ord I i < o

Tactic:
List.SortedGT.lt_ord_of_lt l.2.sortedGT m.2.sortedGT h₁ h₂

Premises used: List.SortedGT.lt_ord_of_lt, List.IsChain.sortedGT, Subtype.property
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hlt : ∀ i ∈ (↑l : List I), ord I i < o
⊢ (π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) l) =
    eval C l

Tactic:
simpa only [← LocallyConstant.coe_inj] using evalFacProp C (ord I · < o) hlt

Premises used: Profinite.NobelingProof.ord, LocallyConstant.coe_inj, LT.lt, Profinite.NobelingProof.Products.evalFacProp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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₁
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)) → ℤ)
⊢ (π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

Tactic:
rw [← LocallyConstant.coe_inj, ← LocallyConstant.toFun_eq_coe]

Premises used: LocallyConstant.coe_inj, LocallyConstant.toFun_eq_coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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₁
⊢ 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:
evalFacProps C (fun (i : I) ↦ ord I i < o₁) (fun (i : I) ↦ ord I i < o₂) hlt
    (fun _ hh ↦ lt_of_lt_of_le hh h)

Premises used: Profinite.NobelingProof.Products.evalFacProps, Profinite.NobelingProof.ord, LT.lt, Profinite.NobelingProof.ProjRestricts, lt_of_lt_of_le
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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₁
⊢ 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:
exact evalFacProps C (fun (i : I) ↦ ord I i < o₁) (fun (i : I) ↦ ord I i < o₂) hlt
    (fun _ hh ↦ lt_of_lt_of_le hh h)

Premises used: Profinite.NobelingProof.Products.evalFacProps, Profinite.NobelingProof.ord, LT.lt, lt_of_lt_of_le
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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
⊢ 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}

Tactic:
ext f
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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) ℤ
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
⊢ 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:
simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]

Premises used: Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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) ℤ
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
⊢ (∃ 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:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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)
⊢ 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

Tactic:
apply and_congr_right

Premises used: and_congr_right
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
h h₁ : eval C m = f ↔ eval C m = f
⊢ 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:
rw [eval_πs C (lt_ord_of_lt hm hl)]

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.lt_ord_of_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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₁
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
⊢ 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}

Tactic:
ext f
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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) ℤ
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
⊢ 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:
simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]

Premises used: Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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) ℤ
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
⊢ (∃ 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:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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)
⊢ 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

Tactic:
apply and_congr_right

Premises used: and_congr_right
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
h₁ h₂ : eval (π C fun (x : I) ↦ ord I x < o₂) m = f ↔ eval (π C fun (x : I) ↦ ord I x < o₂) m = f
⊢ 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:
rw [eval_πs' C h (lt_ord_of_lt hm hl)]

Premises used: Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.Products.lt_ord_of_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
inst_2 : Inhabited I
l : Products I
o : Ordinal.{u}
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hn : (↑l : List I) ≠ []
⊢ ord I (↑l : List I).head! < o

Tactic:
prop_of_isGood C (ord I · < o) h l.val.head! (List.head!_mem_self hn)

Premises used: List.head!_mem_self, List.head!, Profinite.NobelingProof.ord, Profinite.NobelingProof.Products.prop_of_isGood, LT.lt, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
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)
⊢ False

Tactic:
apply hl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h_1 : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
h_2 : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
h : ∀ (x : I), c x = false
⊢ Membership.mem (γ := Set (I → Bool)) {fun (x : I) ↦ false} c

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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
x : I
⊢ c x = false

Tactic:
Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))

Premises used: Iff.mpr, Bool.eq_false_iff, not_lt_zero
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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
x : I
⊢ c x = false

Tactic:
exact Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))

Premises used: Iff.mpr, Bool.eq_false_iff, not_lt_zero
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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 ⊆ {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))
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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}
⊢ C = ∅ ∨ C = {fun (x : I) ↦ false}

Tactic:
rw [Set.subset_singleton_iff_eq] at this

Premises used: Set.subset_singleton_iff_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)
inr : C = {fun (x : I) ↦ false} → LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
cases this
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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 = ∅
inl :
  IsClosed.{u} (X := I → Bool) ∅ →
    ∀ (hsC : contained.{u} (I := I) ∅ 0),
      LinearIndependent.{u, 0, u} (ι := { l : Products I // Products.isGood ∅ l }) ℤ (eval ∅)
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
subst C
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h_1 : IsClosed.{u} (X := I → Bool) ∅
hsC : contained.{u} (I := I) ∅ 0
⊢ LinearIndependent.{u, 0, u} (ι := { l : Products I // Products.isGood ∅ l }) ℤ (eval ∅)

Tactic:
linearIndependentEmpty

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependentEmpty
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h_1 : IsClosed.{u} (X := I → Bool) ∅
hsC : contained.{u} (I := I) ∅ 0
⊢ LinearIndependent.{u, 0, u} (ι := { l : Products I // Products.isGood ∅ l }) ℤ (eval ∅)

Tactic:
exact linearIndependentEmpty

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependentEmpty
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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}
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})
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
subst C