-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem evalFacProp {l : Products I} (J : I → Prop)
    (h : ∀ a, a ∈ l.val → J a) [∀ j, Decidable (J j)] :
    l.eval (π C J) ∘ ProjRestrict C J = l.eval C

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (⇑(eval (π C J) l) ∘ ProjRestrict C J) x = (eval C l) x

Tactic:
dsimp [ProjRestrict]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (eval (π C J) l) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) = (eval C l) x

Proof state:
case h.e_c.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
⊢ (i ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (i ∈ ↑l → ↑x i = true)

Tactic:
apply forall_congr

Result:
case h.e_c.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
⊢ i ∈ ↑l → (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (↑x i = true)

Proof state:
case h.e_c.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
⊢ i ∈ ↑l → (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (↑x i = true)

Tactic:
intro hi

Result:
case h.e_c.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
hi : i ∈ ↑l
⊢ (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (↑x i = true)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
⊢ ⇑(eval (π C J) l) ∘ ProjRestrict C J = ⇑(eval C l)

Tactic:
ext x

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (⇑(eval (π C J) l) ∘ ProjRestrict C J) x = (eval C l) x

Proof state:
case h.e_c
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = ∀ i ∈ ↑l, ↑x i = true

Tactic:
apply forall_congr

Result:
case h.e_c.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ ∀ (a : I), (a ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) a = true) = (a ∈ ↑l → ↑x a = true)

Proof state:
case h.e_c.h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
hi : i ∈ ↑l
⊢ (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (↑x i = true)

Tactic:
simp [h i hi, Proj]

Result:
no goals

Proof state:
case h.e_c.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ ∀ (a : I), (a ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) a = true) = (a ∈ ↑l → ↑x a = true)

Tactic:
intro i

Result:
case h.e_c.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
i : I
⊢ (i ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (i ∈ ↑l → ↑x i = true)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) =
    if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
congr

Result:
case h.e_c
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = ∀ i ∈ ↑l, ↑x i = true

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (eval (π C J) l) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) = (eval C l) x

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

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) =
    if ∀ i ∈ ↑l, ↑x i = true then 1 else 0