-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem C0_projOrd {x : I → Bool} (hx : x ∈ C0 C ho) : Proj (ord I · < o) x = x

Proof state:
case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o = ord I i
⊢ false = x i

Tactic:
simp only [C0, Set.mem_inter_iff, Set.mem_setOf_eq] at hx

Result:
case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
i : I
hi : o = ord I i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
⊢ o ≤ ord I i → false = x i

Tactic:
intro hi

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
⊢ false = x i

Proof state:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
exact (hsC hi).symm

Result:
no goals

Proof state:
case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
i : I
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i

Tactic:
rw [← hx.2, hi]

Result:
no goals

Proof state:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ false = x i

Tactic:
simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC

Result:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i ∨ o = ord I i
⊢ false = x i

Tactic:
rcases hi with hi | hi

Result:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
⊢ false = x i

case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o = ord I i
⊢ false = x i

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
⊢ Proj (fun x => ord I x < o) x i = x i

Tactic:
simp only [Proj, Set.mem_setOf, ite_eq_left_iff, not_lt]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
⊢ o ≤ ord I i → false = x i

Proof state:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ false = x i

Tactic:
rw [← not_imp_not] at hsC

Result:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ false = x i

Proof state:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
⊢ false = x i

Tactic:
specialize hsC x hx.1 i

Result:
case h.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ false = x i

Proof state:
case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
i : I
hi : o = ord I i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i

Tactic:
rw [eq_comm, ord_term ho] at hi

Result:
case h.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
i : I
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
⊢ false = x i

Tactic:
rw [le_iff_lt_or_eq] at hi

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o < ord I i ∨ o = ord I i
⊢ false = x i

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
⊢ Proj (fun x => ord I x < o) x = x

Tactic:
ext i

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
⊢ Proj (fun x => ord I x < o) x i = x i