-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem eval_eq (l : Products I) (x : C) :
    l.eval C x = if ∀ i, i ∈ l.val → (x.val i = true) then 1 else 0

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 1

Tactic:
simp only [List.map_map]

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x) ∘ e C) ↑l).prod = 1

Proof state:
case pos.hl.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
i : I
hi : i ∈ ↑l
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 1

Tactic:
exact if_pos (h i hi)

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_2.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
i : I
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 0 ↔ ↑x i ≠ true

Tactic:
dsimp [LocallyConstant.evalMonoidHom, e]

Result:
case h.e'_2.h.h.e'_2.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
i : I
⊢ (if ↑x i = true then 1 else 0) = 0 ↔ ¬↑x i = true

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 0

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

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Proof state:
case pos.hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ ∀ x_1 ∈ List.map (⇑(LocallyConstant.evalMonoidHom x) ∘ e C) ↑l, x_1 = 1

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

Result:
case pos.hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ ∀ (x_1 : ℤ), (∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = x_1) → x_1 = 1

Proof state:
case pos.hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ ∀ (x_1 : ℤ), (∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = x_1) → x_1 = 1

Tactic:
rintro _ ⟨i, hi, rfl⟩

Result:
case pos.hl.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
i : I
hi : i ∈ ↑l
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 1

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Tactic:
convert h with i

Result:
case h.e'_2.h.h.e'_2.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
i : I
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 0 ↔ ↑x i ≠ true

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (LocallyConstant.evalMonoidHom x) (eval C l) = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
rw [eval, map_list_prod]

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

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

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (LocallyConstant.evalMonoidHom x) (eval C l) = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Proof state:
case h.e'_2.h.h.e'_2.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
i : I
⊢ (if ↑x i = true then 1 else 0) = 0 ↔ ¬↑x i = true

Tactic:
simp only [ite_eq_right_iff, one_ne_zero]

Result:
no goals

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Tactic:
push_neg at h

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 1

case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 0

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x) ∘ e C) ↑l).prod = 1

Tactic:
apply List.prod_eq_one

Result:
case pos.hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ ∀ x_1 ∈ List.map (⇑(LocallyConstant.evalMonoidHom x) ∘ e C) ↑l, x_1 = 1