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

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l = 0

Tactic:
ext ⟨_, _, _, rfl⟩

Result:
case h.mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
w✝ : I → Bool
left✝ : w✝ ∈ C
⊢ (eval (π C J) l) ⟨Proj J w✝, ⋯⟩ = 0 ⟨Proj J w✝, ⋯⟩

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
suffices eval (π C J) l = 0 by
  rw [this]
  exact Submodule.zero_mem _

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l = 0

Proof state:
case h.mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
w✝ : I → Bool
left✝ : w✝ ∈ C
⊢ (eval (π C J) l) ⟨Proj J w✝, ⋯⟩ = 0 ⟨Proj J w✝, ⋯⟩

Tactic:
rw [eval_eq, if_neg fun h ↦ ?_, LocallyConstant.zero_apply]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h✝ : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
w✝ : I → Bool
left✝ : w✝ ∈ C
h : ∀ i ∈ ↑l, ↑⟨Proj J w✝, ⋯⟩ i = true
⊢ False

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ False

Tactic:
apply h

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ 0 ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
exact Submodule.zero_mem _

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h✝ : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
w✝ : I → Bool
left✝ : w✝ ∈ C
h : ∀ i ∈ ↑l, ↑⟨Proj J w✝, ⋯⟩ i = true
⊢ False

Tactic:
simpa [Proj, h'] using h i hi

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
⊢ J i

Tactic:
by_contra h'

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
⊢ False

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

Tactic:
intro i hi

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
⊢ J i

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
rw [this]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ 0 ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})