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
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
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) ⋯) :
        ℤ)
      ((0 : (a : (↑(π C J) : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) ⋯) : ℤ)
⊢ eval (π C J) l = 0

Tactic:
ext ⟨_, _, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
rw :
  ∀ (h : ∀ i ∈ (↑l : List I), (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) ⋯) : I → Bool) i = true),
    False
⊢ 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) ⋯) : ℤ)

Tactic:
rw [eval_eq, if_neg fun h ↦ ?_, LocallyConstant.zero_apply]

Premises used: LocallyConstant.zero_apply, Profinite.NobelingProof.Products.eval_eq, if_neg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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_1 : isGood (π C J) l
i : I
hi : i ∈ (↑l : List I)
h' : ¬J i
w : I → Bool
left : w ∈ C
h : ∀ i ∈ (↑l : List I), (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J w) ⋯) : I → Bool) i = true
⊢ False

Tactic:
simpa [Proj, h'] using h i hi

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
⊢ 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)))

Tactic:
⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans h ?_⟩

Premises used: Profinite.NobelingProof.Products.eval, Membership.mem, Submodule.span_mono, _private.0.Profinite.NobelingProof.GoodProducts.span_iff_products.match_1, Iff.intro, Exists.intro, Set.range, Subtype.val, le_trans
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
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)))
⊢ 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)))

Tactic:
refine ⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans h ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)))
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) ℤ))
⊢ 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:
rw [span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
this : L l
⊢ Products.eval C l ∈
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))

Tactic:
assumption
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
suffices : L l
⊢ Products.eval C l ∈
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))

Tactic:
suffices L l by assumption
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
ind : ∀ (x : Products I), (∀ y < x, L y) → L x
⊢ L l

Tactic:
apply IsWellFounded.induction (· < · : Products I → Products I → Prop)

Premises used: LT.lt, IsWellFounded.induction
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
neg : ∀ (hl : ¬Products.isGood C l), L l
⊢ L l

Tactic:
by_cases hl : l.isGood C

Premises used: Profinite.NobelingProof.Products.isGood
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
pos : Products.eval C l ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)
⊢ L l

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
⊢ Products.eval C l ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)

Tactic:
⟨⟨l, hl⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
⊢ Products.eval C l ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)

Tactic:
exact ⟨⟨l, hl⟩, rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
⊢ 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

Premises used: Profinite.NobelingProof.Products.isGood, Classical.not_not
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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) ℤ))
⊢ 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

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

Tactic:
this hl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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 :
  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)))
⊢ L l

Tactic:
exact this hl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
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) ℤ))
⊢ L l

Tactic:
suffices Products.eval C '' {m | m < l} ⊆ span ℤ (Set.range (GoodProducts.eval C)) by
      rw [← span_le] at this
      exact this hl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
m : Products I
hm : Membership.mem (γ := Set (Products I)) {m : Products I | m < l} m
⊢ Products.eval C m ∈
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))

Tactic:
h m hm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
m : Products I
hm : Membership.mem (γ := Set (Products I)) {m : Products I | m < l} m
⊢ Products.eval C m ∈
    (↑(span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C))) :
      Set (LocallyConstant (↑C : Type u) ℤ))

Tactic:
exact h m hm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ term I ho = i

Tactic:
simp only [term, ord, Ordinal.enum_typein]

Premises used: Ordinal.enum_typein, Profinite.NobelingProof.term, Profinite.NobelingProof.ord
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ ord I (term I ho) = o

Tactic:
simp only [ord, term, Ordinal.typein_enum]

Premises used: Profinite.NobelingProof.term, Ordinal.typein_enum, Profinite.NobelingProof.ord
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
refine_2 : ∀ (h : term I ho = i), ord I i = o
⊢ ord I i = o ↔ term I ho = i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
refine_1 : ∀ (ho : ord I i < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2), term I ho = i
⊢ term I ho = i

Tactic:
subst h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ term I ho = i

Tactic:
term_ord_aux ho

Premises used: Profinite.NobelingProof.term_ord_aux
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ term I ho = i

Tactic:
exact term_ord_aux ho

Premises used: Profinite.NobelingProof.term_ord_aux
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
refine_2 : ord I (term I ho) = o
⊢ ord I i = o

Tactic:
subst h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ ord I (term I ho) = o

Tactic:
ord_term_aux ho

Premises used: Profinite.NobelingProof.ord_term_aux
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ ord I (term I ho) = o

Tactic:
exact ord_term_aux ho

Premises used: Profinite.NobelingProof.ord_term_aux
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
by_contra : ∀ (h' : ¬ord I i < o), False
⊢ ord I i < o

Tactic:
by_contra h'
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
apply :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval C) {m : Products I | m < l})) (eval C l)
⊢ False

Tactic:
apply h
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
this : eval C l = 0
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval C) {m : Products I | m < l})) (eval C l)

Tactic:
simp [this]
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
suffices : eval C l = 0
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval C) {m : Products I | m < l})) (eval C l)

Tactic:
suffices eval C l = 0 by simp [this]
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
h₁ :
  ∀ (x : (↑C : Type u)), Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ) ((0 : (a : (↑C : Type u)) → ℤ) x : ℤ)
⊢ eval C l = 0

Tactic:
ext x
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
x : (↑C : Type u)
h₁ : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) → False
⊢ Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ) ((0 : (a : (↑C : Type u)) → ℤ) x : ℤ)

Tactic:
simp only [eval_eq, LocallyConstant.coe_zero, Pi.zero_apply, ite_eq_right_iff, one_ne_zero]

Premises used: LocallyConstant.coe_zero, Profinite.NobelingProof.Products.eval_eq, Pi.zero_apply, ite_eq_right_iff, one_ne_zero
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
h' : ¬ord I i < o
x : (↑C : Type u)
h₁ : ∀ (h' : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) ∧ True), ord I i < o
⊢ (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) → False

Tactic:
contrapose! h'
-- 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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
x : (↑C : Type u)
h' : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) ∧ True
⊢ ord I i < o

Tactic:
hsC x.val x.prop i (h'.1 i hi)

Premises used: And.left, Subtype.prop, 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 : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ (↑l : List I)
x : (↑C : Type u)
h' : (∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true) ∧ True
⊢ ord I i < o

Tactic:
exact hsC x.val x.prop i (h'.1 i hi)

Premises used: And.left, Subtype.prop, Subtype.val
-- 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
⊢ ∀ (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)
-- 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 ≠ false → ord I i < o), (π C fun (x : I) ↦ ord I x < o) = C
⊢ ∀ (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

Premises used: Bool.not_eq_false, Profinite.NobelingProof.π, ne_eq