-- Mathlib/Topology/Category/Profinite/Nobeling.lean
lemma iso_map_bijective : Function.Bijective (iso_map C J)

Proof state:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
⊢ a = b

Tactic:
ext i

Result:
case refine_1.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
i : I
⊢ ↑a i = ↑b i

Proof state:
case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i

Tactic:
rcases a with ⟨_, c, hc, rfl⟩

Result:
case neg.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
b : ↑(π C J)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) b)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑b i

Proof state:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Function.Bijective ⇑(iso_map C J)

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

Result:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
⊢ a = b

case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ ∃ a_1, (iso_map C J) a_1 = a

Proof state:
case neg.mk.intro.intro.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
d : I → Bool
hd : d ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) ⟨Proj J d, ⋯⟩)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑⟨Proj J d, ⋯⟩ i

Tactic:
simp only [Proj, if_neg hi]

Result:
no goals

Proof state:
case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i => if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩ = a

Tactic:
ext i

Result:
case refine_2.refine_2.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
i : { i // J i }
⊢ ↑((iso_map C J) ⟨fun i => if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩) i = ↑a i

Proof state:
case refine_2.refine_2.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
i : { i // J i }
⊢ ↑((iso_map C J) ⟨fun i => if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩) i = ↑a i

Tactic:
exact dif_pos i.prop

Result:
no goals

Proof state:
case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i => if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

Tactic:
rcases a with ⟨_, y, hy, rfl⟩

Result:
case refine_2.refine_1.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : (i : I) → (fun i => Bool) i
hy : y ∈ C
⊢ (fun i => if hi : J i then ↑⟨(precomp Subtype.val) y, ⋯⟩ ⟨i, hi⟩ else false) ∈ π C J

Proof state:
case refine_1.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
⊢ ↑a i = ↑b i

Tactic:
by_cases hi : J i

Result:
case pos
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : J i
⊢ ↑a i = ↑b i

case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i

Proof state:
case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ ∃ a_1, (iso_map C J) a_1 = a

Tactic:
refine ⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩

Result:
case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i => if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i => if hi : J i then ↑a ⟨i, hi⟩ else false, ?refine_2.refine_1⟩ = a

Proof state:
case refine_1.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
i : I
⊢ ↑a i = ↑b i

Tactic:
rw [Subtype.ext_iff] at h

Result:
case refine_1.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
⊢ ↑a i = ↑b i

Proof state:
case refine_2.refine_1.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : (i : I) → (fun i => Bool) i
hy : y ∈ C
⊢ (fun i => if hi : J i then ↑⟨(precomp Subtype.val) y, ⋯⟩ ⟨i, hi⟩ else false) ∈ π C J

Tactic:
exact ⟨y, hy, rfl⟩

Result:
no goals

Proof state:
case pos
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : J i
⊢ ↑a i = ↑b i

Tactic:
exact congr_fun h ⟨i, hi⟩

Result:
no goals

Proof state:
case neg.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
b : ↑(π C J)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) b)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑b i

Tactic:
rcases b with ⟨_, d, hd, rfl⟩

Result:
case neg.mk.intro.intro.mk.intro.intro
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
d : I → Bool
hd : d ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) ⟨Proj J d, ⋯⟩)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑⟨Proj J d, ⋯⟩ i