awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
rw :
  Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    0
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)

Tactic:
rw [list_prod_apply (π C (· ∈ s)) y _]

Premises used: Profinite.NobelingProof.π, Membership.mem, Profinite.NobelingProof.list_prod_apply
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a :
  Membership.mem (γ := List ℤ)
    (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (factors C s x))
    0
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    0

Tactic:
apply List.prod_eq_zero

Premises used: List.prod_eq_zero
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a :
  ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
⊢ Membership.mem (γ := List ℤ)
    (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (factors C s x))
    0

Tactic:
simp only [List.mem_map]

Premises used: List.mem_map
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
contrapose! : ∀ (h : ∀ (a : I), (↑y : I → Bool) a = (↑x : I → Bool) a), y = x
⊢ ∃ (a : I), (↑y : I → Bool) a ≠ (↑x : I → Bool) a

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h a : ∀ (x_1 : I), (↑y : I → Bool) x_1 = (↑x : I → Bool) x_1
⊢ y = x

Tactic:
ext
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : ∀ (a : I), (↑y : I → Bool) a = (↑x : I → Bool) a
x_1 : I
⊢ (↑y : I → Bool) x_1 = (↑x : I → Bool) x_1

Tactic:
apply h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a :
  ∀ (a : I) (ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a),
    ∃ a ∈ factors C s x,
      Eq (α := ℤ)
        ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
        (0 : ℤ)
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
a₁ :
  ∀ (hx : (↑x : I → Bool) a = false),
    ∃ a ∈ factors C s x,
      Eq (α := ℤ)
        ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
        (0 : ℤ)
a₂ :
  ∀ (hx : (↑x : I → Bool) a = true),
    ∃ a ∈ factors C s x,
      Eq (α := ℤ)
        ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
        (0 : ℤ)
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
cases hx : x.val a

Premises used: Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = false
⊢ (↑y : I → Bool) a = true

Tactic:
rw [hx, ne_eq, Bool.not_eq_false] at ha

Premises used: Bool.not_eq_false, ne_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = false
ha₁ : (↑y : I → Bool) a = true
⊢ (↑x : I → Bool) a = false

Tactic:
rw [hx, ne_eq, Bool.not_eq_false] at ha

Premises used: Bool.not_eq_false, ne_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩

Premises used: Profinite.NobelingProof.π, HSub.hSub, Membership.mem, And.intro, Exists.intro, Profinite.NobelingProof.e, Profinite.NobelingProof.one_sub_e_mem_of_false, OfNat.ofNat
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₄ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₅ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₆ : HSub.hSub (α := ℤ) 1 (if (↑y : I → Bool) a = true then 1 else 0) = 0
a₇ : HSub.hSub (α := ℤ) 1 1 = 0
a₈ a₉ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)

Tactic:
rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]

Premises used: sub_self, LocallyConstant.evalMonoidHom_apply, Pi.one_apply, if_pos, LocallyConstant.coe_mk, LocallyConstant.coe_one, LocallyConstant.sub_apply, Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩

Premises used: Profinite.NobelingProof.π, Membership.mem, Profinite.NobelingProof.e_mem_of_eq_true, And.intro, Exists.intro, Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)

Tactic:
refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
⊢ (↑y : I → Bool) a ≠ true

Tactic:
rw [hx] at ha
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
ha₁ : (↑y : I → Bool) a ≠ true
⊢ (↑x : I → Bool) a = true

Tactic:
rw [hx] at ha
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ true
hx : (↑x : I → Bool) a = true
a₁ : Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) a : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ : Eq (α := ℤ) (if (↑y : I → Bool) a = true then 1 else 0) 0
a₄ a₅ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)

Tactic:
rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]

Premises used: LocallyConstant.evalMonoidHom_apply, LocallyConstant.coe_mk, Profinite.NobelingProof.e, if_neg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h :
  ∀ (y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)),
    Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      ((spanFinBasis C s x : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
⊢ (factors C s x).prod = spanFinBasis C s x

Tactic:
ext y
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h :
  Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    ((spanFinBasis C s x : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)

Tactic:
dsimp [spanFinBasis]

Premises used: Profinite.NobelingProof.spanFinBasis
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
pos :
  ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
neg :
  ∀ (h : ¬y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)

Tactic:
factors_prod_eq_basis_of_eq _ _ h

Premises used: Profinite.NobelingProof.factors_prod_eq_basis_of_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)

Tactic:
exact factors_prod_eq_basis_of_eq _ _ h

Premises used: Profinite.NobelingProof.factors_prod_eq_basis_of_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : ¬y = x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)

Tactic:
factors_prod_eq_basis_of_ne _ _ h

Premises used: Profinite.NobelingProof.factors_prod_eq_basis_of_ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : ¬y = x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)

Tactic:
exact factors_prod_eq_basis_of_ne _ _ h

Premises used: Profinite.NobelingProof.factors_prod_eq_basis_of_ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
pos :
  ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
neg :
  ∀ (h : ¬y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
pos₁ :
  ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
neg₁ :
  ∀ (h : ¬y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)

Tactic:
split_ifs with h <;> [exact factors_prod_eq_basis_of_eq _ _ h;
    exact factors_prod_eq_basis_of_ne _ _ h]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
h :
  ∀ (c_1 : Products I),
    Ne (α := ℤ) ((c : (a : Products I) → ℤ) c_1 : ℤ) (0 : ℤ) →
      Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
        (Submodule.span ℤ
          (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
            {m : Products I | (↑m : List I) ≤ a :: as}))
        (e (π C fun (x : I) ↦ x ∈ s) a *
          HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) c_1 : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) c_1))
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (c.sum fun (a_1 : Products I) (b : ℤ) ↦
      e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1)

Tactic:
apply Submodule.finsuppSum_mem

Premises used: Submodule.finsuppSum_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
⊢ ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    (LinearMap.mulLeft ℤ (e (π C fun (x : I) ↦ x ∈ s) a) :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
        (c • x) =
      HSMul.hSMul (β := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) c
        ((LinearMap.mulLeft ℤ (e (π C fun (x : I) ↦ x ∈ s) a) :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
            x :
          LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)

Tactic:
have hsm := (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)).map_smul
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
h :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ)
      (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m))
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (e (π C fun (x : I) ↦ x ∈ s) a *
      HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) m))

Tactic:
rw [hsm]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
h :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ)
      (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m))

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
h :
  e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m ∈
    Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ a :: as}
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
a₁ : m ∈ (↑c.support : Set (Products I))
⊢ (↑m : List I) ≤ as

Tactic:
apply hc
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ m ∈ (↑c.support : Set (Products I))

Tactic:
simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

Premises used: Finsupp.mem_support_iff, Finset.mem_coe