-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem factors_prod_eq_basis_of_ne {x y : (π C (· ∈ s))} (h : y ≠ x) :
    (factors C s x).prod y = 0

Proof state:
case a.intro.false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

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

Result:
case a.intro.false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Proof state:
case a.intro.true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x => x ∈ s) a) = 0

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

Result:
no goals

Proof state:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply h

Result:
case a.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Proof state:
case a.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝

Tactic:
apply h

Result:
no goals

Proof state:
case a.intro.false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ (LocallyConstant.evalMonoidHom y) (1 - e (π C fun x => 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]

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x

Tactic:
ext

Result:
case a.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝

Proof state:
case a.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
cases hx : x.val a

Result:
case a.intro.false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

case a.intro.true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ ∃ a, ↑y a ≠ ↑x a

Tactic:
contrapose! h

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x

Proof state:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ 0 ∈ List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)

Tactic:
simp only [List.mem_map]

Result:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Proof state:
case a.intro.true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x => x ∈ s) a) = 0

Tactic:
rw [hx] at ha

Result:
case a.intro.true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x => x ∈ s) a) = 0

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 0

Tactic:
apply List.prod_eq_zero

Result:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y ≠ x
⊢ 0 ∈ List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)