-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem proj_eq_of_subset (h : ∀ i, J i → K i) : π (π C K) J = π C J

Proof state:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J '' (Proj K '' C)

Tactic:
rw [← Set.image_comp]

Result:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J ∘ Proj K '' C

Proof state:
case h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
⊢ x ∈ π (π C K) J ↔ x ∈ π C J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
⊢ x ∈ π C J

case h.refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J

Proof state:
case h.refine_1.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J z = (Proj J ∘ Proj K) z

Tactic:
rw [proj_comp_of_subset J K h]

Result:
no goals

Proof state:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ (Proj J ∘ Proj K) y = Proj J y

Tactic:
rw [proj_comp_of_subset J K h]

Result:
no goals

Proof state:
case h.refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J

Tactic:
obtain ⟨y, hy, rfl⟩ := h

Result:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ π (π C K) J

Proof state:
case h.refine_1.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J (Proj K z) ∈ π C J

Tactic:
refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩

Result:
case h.refine_1.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J z = (Proj J ∘ Proj K) z

Proof state:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ π (π C K) J = π C J

Tactic:
ext x

Result:
case h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
⊢ x ∈ π (π C K) J ↔ x ∈ π C J

Proof state:
case h.refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
⊢ x ∈ π C J

Tactic:
obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h

Result:
case h.refine_1.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J (Proj K z) ∈ π C J

Proof state:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ π (π C K) J

Tactic:
dsimp [π]

Result:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J '' (Proj K '' C)

Proof state:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J ∘ Proj K '' C

Tactic:
refine ⟨y, hy, ?_⟩

Result:
case h.refine_2.intro.intro
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ (Proj J ∘ Proj K) y = Proj J y