awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
⊢ SwapTrue o
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
            (Proj (fun (x : I) ↦ ord I x < o) g) ⋯) :
        I → Bool) ∈
    C1 C ho
have h : SwapTrue o
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
          (Proj (fun (x : I) ↦ ord I x < o) g) sorry) :
      I → Bool) =
  g
Tactic: convert! hg
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
⊢ (fun (i : I) ↦ if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g
have h : ∀ (i : I), (if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
⊢ (if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g i
have pos : ∀ (h : ord I i = o), true = g i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
pos : ∀ (h : ord I i = o), true = g i
⊢ (if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g i
have neg : ∀ (h : ¬ord I i = o), Proj (fun (x : I) ↦ ord I x < o) g i = g i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i
have h₁ : term I ho = i
Tactic: rw [ord_term ho] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun (x : I) ↦ ord I x < o) g i = g i
have neg : o ≤ ord I i → ¬g i = true
Tactic: simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ o ≤ ord I i → ¬g i = true
have hsC₁ : g i = true → ord I i < Order.succ o
Tactic: specialize hsC g hg.1 i
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
hsC : g i = true → ord I i < Order.succ o
h' : o ≤ ord I i
⊢ ¬g i = true
have neg : ∀ (hsC : g i = true), g i = true ∧ Order.succ o ≤ ord I i
Tactic: contrapose! hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
⊢ Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        ((πs C o :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          y) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (0 : LocallyConstant (↑(C' C ho) : Type u) ℤ)
have h : ∀ (x : (↑(C' C ho) : Type u)),
  Eq (α := ℤ)
    ((((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                y) :
            LocallyConstant (↑(C' C ho) : Type u) ℤ) :
          (a : (↑(C' C ho) : Type u)) → ℤ)
        x :
      ℤ)
    ((0 : (a : (↑(C' C ho) : Type u)) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
⊢ Eq (α := ℤ)
    ((((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                y) :
            LocallyConstant (↑(C' C ho) : Type u) ℤ) :
          (a : (↑(C' C ho) : Type u)) → ℤ)
        x :
      ℤ)
    ((0 : (a : (↑(C' C ho) : Type u)) → ℤ) x : ℤ)
have h : HSub.hSub (α := ℤ) (β := ℤ)
    ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) :
      ℤ)
    ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) :
      ℤ) =
  0
Tactic: dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁, LocallyConstant.sub_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
          (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) :
        ℤ)
      ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
          (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) :
        ℤ) =
    0
have h : Eq (α := ℤ)
  ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
      (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) :
    ℤ)
  ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
      (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) :
    ℤ)
Tactic: simp only [sub_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
⊢ Eq (α := ℤ)
    ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) :
      ℤ)
    ((y : (a : (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) :
      ℤ)
have h : Eq (α := (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x))
  (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
⊢ Eq (α := (↑(π C fun (x : I) ↦ ord I x < o) : Type u)) (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x))
    (ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x))
have h : ∀ (i : I),
  (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) : I → Bool) i =
    (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) : I → Bool) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
i : I
⊢ (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₁ C hsC ho x)) : I → Bool) i =
    (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (CC'₀ C ho x)) : I → Bool) i
have h : (if ord I i < o then SwapTrue o (↑x : I → Bool) i else false) = if ord I i < o then (↑x : I → Bool) i else false
Tactic: dsimp [CC'₀, CC'₁, ProjRestrict, Proj]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
i : I
⊢ (if ord I i < o then SwapTrue o (↑x : I → Bool) i else false) = if ord I i < o then (↑x : I → Bool) i else false
have apply : ord I i < o → SwapTrue o (↑x : I → Bool) i = (↑x : I → Bool) i
Tactic: apply if_ctx_congr Iff.rfl _ (fun _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
x : (↑(C' C ho) : Type u)
i : I
⊢ ord I i < o → SwapTrue o (↑x : I → Bool) i = (↑x : I → Bool) i
have simp : ord I i < o → ord I i = o → true = (↑x : I → Bool) i
Tactic: simp only [SwapTrue, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
⊢ Proj (fun (x : I) ↦ ord I x < o) x = x
have h : ∀ (i : I), Proj (fun (x : I) ↦ ord I x < o) x i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
⊢ Proj (fun (x : I) ↦ ord I x < o) x i = x i
have h : o ≤ ord I i → false = x i
Tactic: simp only [Proj, ite_eq_left_iff, not_lt]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
⊢ false = x i
have h : ∀ (hi : o < ord I i), false = x i
Tactic: rcases hi.lt_or_eq with hi | hi
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
h : ∀ (hi : o < ord I i), false = x i
⊢ false = x i
have h₁ : ∀ (hi : o = ord I i), false = x i
Tactic: rcases hi.lt_or_eq with hi | hi
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
⊢ false = x i
have hsC₁ : x i = true → ord I i < Order.succ o
Tactic: specialize hsC x hx.1 i
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ false = x i
have hsC₁ : ¬ord I i < Order.succ o → ¬x i = true
Tactic: rw [← not_imp_not] at hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ false = x i
have hsC₁ : o < ord I i → x i = false
Tactic: simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o = ord I i
⊢ false = x i
have hx₁ : x ∈ C ∧ x (term I ho) = false
Tactic: simp only [C0, Set.mem_inter_iff, Set.mem_setOf_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : o = ord I i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i
have hi₁ : term I ho = i
Tactic: rw [eq_comm, ord_term ho] at hi
Cleared hypotheses: hi, hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ false = x i
have h : x (term I ho) = x i
Tactic: rw [← hx.2, hi]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
h : x (term I ho) = x i
⊢ false = x i
have h₁ : x i = x i
Tactic: rw [← hx.2, hi]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
⊢ SwapTrue o (Proj (fun (x : I) ↦ ord I x < o) x) = x
have h : ∀ (i : I), SwapTrue o (Proj (fun (x : I) ↦ ord I x < o) x) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
⊢ (if ord I i = o then true else if ord I i < o then x i else false) = x i
have pos : ∀ (hi : ord I i = o), true = x i
Tactic: split_ifs with hi h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
pos : ∀ (hi : ord I i = o), true = x i
⊢ (if ord I i = o then true else if ord I i < o then x i else false) = x i
have pos₁ : ∀ (hi : ¬ord I i = o) (h : ord I i < o), x i = x i
Tactic: split_ifs with hi h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
pos : ∀ (hi : ord I i = o), true = x i
pos₁ : ∀ (hi : ¬ord I i = o) (h : ord I i < o), x i = x i
⊢ (if ord I i = o then true else if ord I i < o then x i else false) = x i
have neg : ∀ (hi : ¬ord I i = o) (h : ¬ord I i < o), false = x i
Tactic: split_ifs with hi h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ true = x i
have hi₁ : term I ho = i
Tactic: rw [ord_term ho] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
⊢ true = x i
have pos : x (term I ho) = x i
Tactic: rw [← hx.2, hi]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
pos : x (term I ho) = x i
⊢ true = x i
have pos₁ : x i = x i
Tactic: rw [← hx.2, hi]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i
have h₁ : o ≤ ord I i
Tactic: simp only [not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
⊢ false = x i
have h' : o < ord I i
Tactic: have h' : o < ord I i := lt_of_le_of_ne h (Ne.symm hi)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i
have hsC₁ : x i = true → ord I i < Order.succ o
Tactic: specialize hsC x hx.1 i
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ false = x i
have hsC₁ : ¬ord I i < Order.succ o → ¬x i = true
Tactic: rw [← not_imp_not] at hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ false = x i
have hsC₁ : o < ord I i → x i = false
Tactic: simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
f : LocallyConstant (↑C : Type u) ℤ
hf :
  HSub.hSub (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ)
      ((LocallyConstant.comapₗ ℤ
              { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ : C((↑(C' C ho) : Type u), (↑C : Type u)) } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
      ((LocallyConstant.comapₗ ℤ
              { toFun := CC'₀ C ho, continuous_toFun := ⋯ : C((↑(C' C ho) : Type u), (↑C : Type u)) } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    0
⊢ ∃ (y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have hf₁ : Eq (α := (a : (↑(C' C ho) : Type u)) → ℤ)
  (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := sorry } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) :
    (a : (↑(C' C ho) : Type u)) → ℤ)
  (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := sorry } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) :
    (a : (↑(C' C ho) : Type u)) → ℤ)
Tactic: simp only [sub_eq_zero, ← LocallyConstant.coe_inj] at hf
Cleared hypotheses: hf