-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem range_equiv_smaller_toFun_bijective (o : Ordinal) :
    Function.Bijective (range_equiv_smaller_toFun C o)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
hb : b ∈ range (π C fun x => ord I x < o) ∧ (πs C o) b = a
⊢ (fun x => ⟨(πs C o) ↑x, ⋯⟩) ⟨b, ⋯⟩ = ⟨a, ⋯⟩

Tactic:
simpa only [Subtype.mk.injEq] using hb.2

Result:
no goals

Proof state:
case refine_1.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (πs C o) ↑a = (πs C o) ↑b
⊢ ↑a = ↑b

Tactic:
exact injective_πs C o hab

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective fun x => ⟨(πs C o) ↑x, ⋯⟩

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

Result:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (fun x => ⟨(πs C o) ↑x, ⋯⟩) a = (fun x => ⟨(πs C o) ↑x, ⋯⟩) b
⊢ a = b

case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
hb : b ∈ range (π C fun x => ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x => ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Proof state:
case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
hb : b ∈ range (π C fun x => ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x => ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Tactic:
use ⟨b, hb.1⟩

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
hb : b ∈ range (π C fun x => ord I x < o) ∧ (πs C o) b = a
⊢ (fun x => ⟨(πs C o) ↑x, ⋯⟩) ⟨b, ⋯⟩ = ⟨a, ⋯⟩

Proof state:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (fun x => ⟨(πs C o) ↑x, ⋯⟩) a = (fun x => ⟨(πs C o) ↑x, ⋯⟩) b
⊢ a = b

Tactic:
ext1

Result:
case refine_1.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (fun x => ⟨(πs C o) ↑x, ⋯⟩) a = (fun x => ⟨(πs C o) ↑x, ⋯⟩) b
⊢ ↑a = ↑b

Proof state:
case refine_1.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (fun x => ⟨(πs C o) ↑x, ⋯⟩) a = (fun x => ⟨(πs C o) ↑x, ⋯⟩) b
⊢ ↑a = ↑b

Tactic:
simp only [Subtype.mk.injEq] at hab

Result:
case refine_1.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x => ord I x < o))
hab : (πs C o) ↑a = (πs C o) ↑b
⊢ ↑a = ↑b

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective (range_equiv_smaller_toFun C o)

Tactic:
dsimp (config := { unfoldPartialApp := true }) [range_equiv_smaller_toFun]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective fun x => ⟨(πs C o) ↑x, ⋯⟩