-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.P0 : P I 0 := fun _ C _ hsC ↦ by
  have : C ⊆ {(fun _ ↦ false)} := fun c hc ↦ by
    ext x; exact Bool.eq_false_iff.mpr (fun ht ↦ (Ordinal.not_lt_zero (ord I x)) (hsC c hc x ht))
  rw [Set.subset_singleton_iff_eq] at this
  cases this
  · subst C
    exact linearIndependentEmpty
  · subst C
    exact linearIndependentSingleton

Proof state:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false

Tactic:
exact Bool.eq_false_iff.mpr (fun ht ↦ (Ordinal.not_lt_zero (ord I x)) (hsC c hc x ht))

Result:
no goals

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C ⊆ {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Tactic:
rw [Set.subset_singleton_iff_eq] at this

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
⊢ c ∈ {fun x => false}

Tactic:
ext x

Result:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false

Proof state:
case inr
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
x✝ : IsClosed {fun x => false}
hsC : contained {fun x => false} 0
⊢ LinearIndependent ℤ (eval {fun x => false})

Tactic:
exact linearIndependentSingleton

Result:
no goals

Proof state:
case inr
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
h✝ : C = {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Tactic:
subst C

Result:
case inr
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
x✝ : IsClosed {fun x => false}
hsC : contained {fun x => false} 0
⊢ LinearIndependent ℤ (eval {fun x => false})

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
⊢ LinearIndependent ℤ (eval C)

Tactic:
have : C ⊆ {(fun _ ↦ false)} := fun c hc ↦ by
  ext x; exact Bool.eq_false_iff.mpr (fun ht ↦ (Ordinal.not_lt_zero (ord I x)) (hsC c hc x ht))

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C ⊆ {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Proof state:
case inl
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
h✝ : C = ∅
⊢ LinearIndependent ℤ (eval C)

Tactic:
subst C

Result:
case inl
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
x✝ : IsClosed ∅
hsC : contained ∅ 0
⊢ LinearIndependent ℤ (eval ∅)

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Tactic:
cases this

Result:
case inl
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
h✝ : C = ∅
⊢ LinearIndependent ℤ (eval C)

case inr
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
h✝ : C = {fun x => false}
⊢ LinearIndependent ℤ (eval C)

Proof state:
case inl
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 => x1 < x2
x✝ : IsClosed ∅
hsC : contained ∅ 0
⊢ LinearIndependent ℤ (eval ∅)

Tactic:
exact linearIndependentEmpty

Result:
no goals