-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem factors_prod_eq_basis_of_eq {x y : (π C fun x ↦ x ∈ s)} (h : y = x) :
    (factors C s x).prod y = 1

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ↑x b = true
⊢ (e (π C fun x => x ∈ s) b) x = 1

Tactic:
rw [e, LocallyConstant.coe_mk, if_pos hh]

Result:
no goals

Proof state:
case hl.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
⊢ ((Pi.evalMonoidHom (fun a => ℤ) x).comp LocallyConstant.coeFnMonoidHom)
      (if ↑x b = true then e (π C fun x => x ∈ s) b else 1 - e (π C fun x => x ∈ s) b) =
    1

Tactic:
dsimp

Result:
case hl.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
⊢ (if ↑x b = true then e (π C fun x => x ∈ s) b else 1 - e (π C fun x => x ∈ s) b) x = 1

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1

Tactic:
simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

Result:
no goals

Proof state:
case hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
⊢ ∀ (x_1 : ℤ),
    (∃ a,
        (∃ a_1 ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s,
            (if ↑x a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) = a) ∧
          ((Pi.evalMonoidHom (fun a => ℤ) x).comp LocallyConstant.coeFnMonoidHom) a = x_1) →
      x_1 = 1

Tactic:
rintro _ ⟨a, ⟨b, _, rfl⟩, rfl⟩

Result:
case hl.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
⊢ ((Pi.evalMonoidHom (fun a => ℤ) x).comp LocallyConstant.coeFnMonoidHom)
      (if ↑x b = true then e (π C fun x => x ∈ s) b else 1 - e (π C fun x => x ∈ s) b) =
    1

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 = 1

Tactic:
apply List.prod_eq_one

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

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

Tactic:
simp only [h, List.mem_map, LocallyConstant.evalMonoidHom, factors]

Result:
case hl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
⊢ ∀ (x_1 : ℤ),
    (∃ a,
        (∃ a_1 ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s,
            (if ↑x a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) = a) ∧
          ((Pi.evalMonoidHom (fun a => ℤ) x).comp LocallyConstant.coeFnMonoidHom) a = x_1) →
      x_1 = 1

Proof state:
case hl.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
⊢ (if ↑x b = true then e (π C fun x => x ∈ s) b else 1 - e (π C fun x => x ∈ s) b) x = 1

Tactic:
split_ifs with hh

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ↑x b = true
⊢ (e (π C fun x => x ∈ s) b) x = 1

case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ¬↑x b = true
⊢ (1 - e (π C fun x => x ∈ s) b) x = 1

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ¬↑x b = true
⊢ (1 - e (π C fun x => x ∈ s) b) x = 1

Tactic:
rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
h : y = x
b : I
left✝ : b ∈ Finset.sort (fun x1 x2 => x1 ≥ x2) s
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1