-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem CC_comp_zero : ∀ y, (Linear_CC' C hsC ho) ((πs C o) y) = 0

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ((Linear_CC' C hsC ho) ((πs C o) y)) x = 0 x

Tactic:
dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁, LocallyConstant.sub_apply]

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) -
      y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)) =
    0

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
⊢ ∀ (y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ), (Linear_CC' C hsC ho) ((πs C o) y) = 0

Tactic:
intro y

Result:
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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
⊢ (Linear_CC' C hsC ho) ((πs C o) y) = 0

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = ↑x i

Tactic:
exact (h₁.ne h₂).elim

Result:
no goals

Proof state:
case h.h.e_6.h.a.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ↑(ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) i =
    ↑(ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)) i

Tactic:
dsimp [CC'₀, CC'₁, ProjRestrict, Proj]

Result:
case h.h.e_6.h.a.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ (if ord I i < o then SwapTrue o (↑x) i else false) = if ord I i < o then ↑x i else false

Proof state:
case h.h.e_6.h.a.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ (if ord I i < o then SwapTrue o (↑x) i else false) = if ord I i < o then ↑x i else false

Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ ↦ rfl)

Result:
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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → SwapTrue o (↑x) i = ↑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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → SwapTrue o (↑x) i = ↑x i

Tactic:
simp only [SwapTrue, ite_eq_right_iff]

Result:
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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → ord I i = o → true = ↑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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) -
      y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)) =
    0

Tactic:
simp only [Pi.zero_apply, sub_eq_zero]

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) = y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x))

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) = y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x))

Tactic:
congr 1

Result:
case h.h.e_6.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x) = ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)

Proof state:
case h.h.e_6.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x) = ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)

Tactic:
ext i

Result:
case h.h.e_6.h.a.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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ↑(ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) i =
    ↑(ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho 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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
⊢ (Linear_CC' C hsC ho) ((πs C o) y) = 0

Tactic:
ext x

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ((Linear_CC' C hsC ho) ((πs C o) y)) x = 0 x

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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → ord I i = o → true = ↑x i

Tactic:
intro h₁ h₂

Result:
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
y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = ↑x i