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
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
inr :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C a)
⊢ False

Tactic:
apply ha
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
inr :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C b)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C a)

Tactic:
rw [h]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C b)

Tactic:
Submodule.subset_span ⟨b, h', rfl⟩

Premises used: And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C b)

Tactic:
exact Submodule.subset_span ⟨b, h', rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
⊢ Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha <
      Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb ∨
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb <
      Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha

Tactic:
cases hne.lt_or_gt with
  | inl h' => apply hb; rw [← h]; exact Submodule.subset_span ⟨a, h', rfl⟩
  | inr h' => apply ha; rw [h]; exact Submodule.subset_span ⟨b, h', rfl⟩

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
⊢ Eq (α := (↑(GoodProducts C) : Type u) → (↑(range C) : Type u)) (Equiv.toFun (equiv_range C))
    (Set.rangeFactorization (eval C))

Tactic:
rfl

Premises used: Profinite.NobelingProof.Products.isGood, Set.Mem, setOf, Profinite.NobelingProof.GoodProducts, Set.rangeFactorization, Not, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ
      (Subtype.val (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦
          x ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)) ∘
        Equiv.toFun (equiv_range C)) ↔
    LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ) fun (p : (↑(range C) : Type u)) ↦
      (↑p : LocallyConstant (↑C : Type u) ℤ)

Tactic:
linearIndependent_equiv (equiv_range C)

Premises used: Profinite.NobelingProof.Products.isGood, Profinite.NobelingProof.GoodProducts.equiv_range, Set.Mem, setOf, linearIndependent_equiv, Profinite.NobelingProof.GoodProducts, Not, Profinite.NobelingProof.GoodProducts.range
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ
      (Subtype.val (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦
          x ∈ Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)) ∘
        Equiv.toFun (equiv_range C)) ↔
    LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ) fun (p : (↑(range C) : Type u)) ↦
      (↑p : LocallyConstant (↑C : Type u) ℤ)

Tactic:
exact linearIndependent_equiv (equiv_range C)

Premises used: Profinite.NobelingProof.GoodProducts.equiv_range, linearIndependent_equiv
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
change :
  Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (eval C l) : ℤ)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)

Tactic:
change LocallyConstant.evalMonoidHom x (l.eval C) = _

Premises used: Profinite.NobelingProof.Products.eval, DFunLike.coe, LocallyConstant.evalMonoidHom
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
rw :
  Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (eval C l) : ℤ)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)

Tactic:
rw [eval, map_list_prod]

Premises used: Profinite.NobelingProof.Products.eval, map_list_prod
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
pos :
  ∀ (h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true),
    Eq (α := ℤ)
      (List.prod
        (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
          (List.map (e C) (↑l : List I))))
      1
neg :
  ∀ (h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true),
    Eq (α := ℤ)
      (List.prod
        (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
          (List.map (e C) (↑l : List I))))
      0
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
pos :
  Eq (α := ℤ)
    (List.prod
      (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C) (↑l : List I)))
    1
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    1

Tactic:
simp only [List.map_map]

Premises used: List.map_map
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
pos :
  ∀ (x_1 : ℤ),
    Membership.mem (γ := List ℤ)
        (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C)
          (↑l : List I))
        x_1 →
      x_1 = 1
⊢ Eq (α := ℤ)
    (List.prod
      (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C) (↑l : List I)))
    1

Tactic:
apply List.prod_eq_one

Premises used: List.prod_eq_one
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
pos :
  ∀ (x_1 : ℤ),
    (∃ a ∈ (↑l : List I), (LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) = x_1) →
      x_1 = 1
⊢ ∀ (x_1 : ℤ),
    Membership.mem (γ := List ℤ)
        (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C)
          (↑l : List I))
        x_1 →
      x_1 = 1

Tactic:
simp only [List.mem_map, Function.comp_apply]

Premises used: Function.comp_apply, List.mem_map
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l : List I)
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (1 : ℤ)

Tactic:
if_pos (h i hi)

Premises used: if_pos, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l : List I)
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (1 : ℤ)

Tactic:
exact if_pos (h i hi)

Premises used: if_pos
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
neg :
  ∃ a ∈ (↑l : List I),
    Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    0

Tactic:
simp only [List.map_map, List.prod_eq_zero_iff, List.mem_map, Function.comp_apply]

Premises used: List.map_map, List.prod_eq_zero_iff, Function.comp_apply, List.mem_map
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
⊢ ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true

Tactic:
h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
h₁ :
  ∀ (i : I),
    Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (0 : ℤ) ↔
      (↑x : I → Bool) i ≠ true
⊢ ∃ a ∈ (↑l : List I),
    Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) : ℤ) (0 : ℤ)

Tactic:
convert! h with i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
i : I
h₁ : Eq (α := ℤ) (if (↑x : I → Bool) i = true then 1 else 0) 0 ↔ ¬(↑x : I → Bool) i = true
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (0 : ℤ) ↔
    (↑x : I → Bool) i ≠ true

Tactic:
dsimp [LocallyConstant.evalMonoidHom, e]

Premises used: Profinite.NobelingProof.e, LocallyConstant.evalMonoidHom
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
i : I
⊢ Eq (α := ℤ) (if (↑x : I → Bool) i = true then 1 else 0) 0 ↔ ¬(↑x : I → Bool) i = true

Tactic:
simp only [ite_eq_right_iff, one_ne_zero]

Premises used: 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
l : Products I
J : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
h₁ :
  ∀ (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 : ℤ)
⊢ Eq (α := (↑C : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ) (ProjRestrict C J))
    (⇑(eval C l) : (a : (↑C : Type u)) → ℤ)

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
h₁ :
  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 : ℤ)
⊢ 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 : ℤ)

Tactic:
dsimp [ProjRestrict]

Premises used: Profinite.NobelingProof.ProjRestrict
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
h₁ :
  Eq (α := ℤ)
    (if ∀ i ∈ (↑l : List I), (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) : I → Bool) i = true then 1 else 0)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
⊢ 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 : ℤ)

Tactic:
rw [Products.eval_eq, Products.eval_eq]

Premises used: Profinite.NobelingProof.Products.eval_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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 (α := ℤ)
    (if ∀ i ∈ (↑l : List I), (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) : I → Bool) i = true then 1 else 0)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)

Tactic:
simp +contextual [h, Proj]

Premises used: Profinite.NobelingProof.Proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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) ⋯) :
            (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
          x :
        ℤ)
      ((eval (π (π C K) J) l : (a : (↑(π (π C K) J) : Type u)) → ℤ) x : ℤ)
⊢ 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)) → ℤ)

Tactic:
ext
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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) ⋯) :
          (a : (↑(π (π C K) J) : Type u)) → (↑(π C J) : Type u))
        x :
      ℤ)
    ((eval (π (π C K) J) l : (a : (↑(π (π C K) J) : Type u)) → ℤ) x : ℤ)

Tactic:
simp [Homeomorph.setCongr, Products.eval_eq]

Premises used: Profinite.NobelingProof.Products.eval_eq, Homeomorph.setCongr
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)) → ℤ)

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]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)) → ℤ)
rw₃ 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))
⊢ 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)) → ℤ)

Tactic:
rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]

Premises used: Profinite.NobelingProof.π, Profinite.NobelingProof.ProjRestricts, Profinite.NobelingProof.Products.evalFacProp, Function.comp_assoc
-- 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)
by_contra : ∀ (h' : ¬J i), False
⊢ J i

Tactic:
by_contra h'
-- 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
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)
⊢ False

Tactic:
apply h
-- 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
this : eval (π C J) l = 0
rw :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C J) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C J)) {m : Products I | m < 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)

Tactic:
rw [this]
-- 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
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})) 0

Tactic:
Submodule.zero_mem _

Premises used: Set.Mem, Submodule.zero_mem
-- 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
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})) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- 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
suffices : 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)

Tactic:
suffices eval (π C J) l = 0 by
    rw [this]
    exact Submodule.zero_mem _