awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ
h :
  Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)
m : { l : Products I // Products.isGood (π C fun (x : I) ↦ x ∈ K) l }
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (Set.range (ι := Products I) (Products.eval C))
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ x ∈ K) m) :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
⟨m.val, eval_eq_πJ C K m.val m.prop⟩

Premises used: Set.Mem, setOf, Subtype.prop, Exists.intro, Profinite.NobelingProof.eval_eq_πJ, Set.range, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ
h :
  Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)
m : { l : Products I // Products.isGood (π C fun (x : I) ↦ x ∈ K) l }
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (Set.range (ι := Products I) (Products.eval C))
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ x ∈ K) m) :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
exact ⟨m.val, eval_eq_πJ C K m.val m.prop⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed (C0 C ho)

Tactic:
hC.inter ?_

Premises used: Profinite.NobelingProof.C0, IsClosed.inter
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
refine : IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = false}
⊢ IsClosed (C0 C ho)

Tactic:
refine hC.inter ?_

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)

Tactic:
have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = false}

Tactic:
IsClosed.preimage h (t := {false}) (isClosed_discrete _)

Premises used: Set.Mem, setOf, isClosed_discrete, Set.preimage, Set.singleton, IsClosed.preimage
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = false}

Tactic:
exact IsClosed.preimage h (t := {false}) (isClosed_discrete _)

Premises used: isClosed_discrete, IsClosed.preimage
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed (C1 C ho)

Tactic:
hC.inter ?_

Premises used: Profinite.NobelingProof.C1, IsClosed.inter
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
refine : IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = true}
⊢ IsClosed (C1 C ho)

Tactic:
refine hC.inter ?_

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = true}

Tactic:
IsClosed.preimage h (t := {true}) (isClosed_discrete _)

Premises used: Set.Mem, setOf, isClosed_discrete, Set.preimage, Set.singleton, IsClosed.preimage
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = true}

Tactic:
exact IsClosed.preimage h (t := {true}) (isClosed_discrete _)

Premises used: isClosed_discrete, IsClosed.preimage
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ contained (π (C1 C ho) fun (x : I) ↦ ord I x < o) o

Tactic:
contained_proj _ _

Premises used: Profinite.NobelingProof.contained_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h : ∀ (x : I → Bool), x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C
⊢ C0 C ho ∪ C1 C ho = C

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C

Tactic:
simp only [C0, C1, Set.mem_union, Set.mem_inter_iff, Set.mem_setOf_eq,
    ← and_or_left, and_iff_left_iff_imp, Bool.dichotomy (x (term I ho)), implies_true]

Premises used: Set.mem_union, and_or_left, Profinite.NobelingProof.C0, Set.mem_inter_iff, Profinite.NobelingProof.C1, Set.mem_setOf_eq, Profinite.NobelingProof.term, Bool.dichotomy, implies_true, and_iff_left_iff_imp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed (C' C ho)

Tactic:
IsClosed.inter (isClosed_C0 _ hC _) (isClosed_proj _ _ (isClosed_C1 _ hC _))

Premises used: Profinite.NobelingProof.isClosed_C0, Profinite.NobelingProof.isClosed_proj, IsClosed.inter, Profinite.NobelingProof.C', Profinite.NobelingProof.isClosed_C1
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ contained (C' C ho) o

Tactic:
fun f hf i hi ↦ contained_C1 C ho f hf.2 i hi

Premises used: Profinite.NobelingProof.contained_C1, And.right, Profinite.NobelingProof.contained
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
h : ∀ (i : I), Continuous (Y := Bool) fun (a : I → Bool) ↦ if ord I i = o then true else a i
⊢ Continuous (Y := I → Bool) fun (f : I → Bool) (i : I) ↦ if ord I i = o then true else f i

Tactic:
apply continuous_pi

Premises used: continuous_pi
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
i : I
h : Continuous (ite (ord I i = o) true)
h₁ : Continuous (Y := Bool) fun (x : I → Bool) ↦ x i
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if ord I i = o then true else a i

Tactic:
apply Continuous.comp'

Premises used: Continuous.comp'
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

Tactic:
apply continuous_bot

Premises used: continuous_bot
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (Y := Bool) fun (x : I → Bool) ↦ x i

Tactic:
apply continuous_apply

Premises used: continuous_apply
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
f : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)
obtain :
  ∀ (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
⊢ SwapTrue o (↑f : I → Bool) ∈ C1 C ho

Tactic:
obtain ⟨f, g, hg, rfl⟩ := f

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ g ∈ C1 C ho

Tactic:
hg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
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) ⋯) :
        I → Bool) =
    g
⊢ 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

Tactic:
convert! hg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h : ∀ (i : I), (if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g i
⊢ (fun (i : I) ↦ if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g

Tactic:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
neg : ∀ (h : ¬ord I i = o), Proj (fun (x : I) ↦ ord I x < o) g i = g i
⊢ (if ord I i = o then true else Proj (fun (x : I) ↦ ord I x < o) g i) = g i

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ term I ho = i

Tactic:
rw [ord_term ho] at h

Premises used: Profinite.NobelingProof.ord_term
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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 : term I ho = i
⊢ true = g i

Tactic:
simpa only [← h] using hg.2.symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
neg : o ≤ ord I i → ¬g i = true
⊢ Proj (fun (x : I) ↦ ord I x < o) g i = g i

Tactic:
simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]

Premises used: ite_eq_left_iff, Profinite.NobelingProof.Proj, eq_comm, not_lt, Bool.not_eq_true
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ g i = true → ord I i < Order.succ o

Tactic:
specialize hsC g hg.1 i

Premises used: And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
neg : ∀ (hsC : g i = true), g i = true ∧ Order.succ o ≤ ord I i
⊢ ¬g i = true

Tactic:
contrapose! hsC
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h' : o ≤ ord I i
hsC : g i = true
⊢ g i = true ∧ Order.succ o ≤ ord I i

Tactic:
⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩

Premises used: Order.succ_le_of_lt, And.intro, LE.le.lt_of_ne'
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h' : o ≤ ord I i
hsC : g i = true
⊢ g i = true ∧ Order.succ o ≤ ord I i

Tactic:
exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ Continuous (X := (↑(C' C ho) : Type u)) (CC'₀ C ho)

Tactic:
Continuous.subtype_mk continuous_subtype_val _

Premises used: continuous_subtype_val, Continuous.subtype_mk, Profinite.NobelingProof.CC'₀
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
⊢ Continuous (CC'₁ C hsC ho)

Tactic:
Continuous.subtype_mk (Continuous.comp (continuous_swapTrue o) continuous_subtype_val) _

Premises used: continuous_subtype_val, Continuous.comp, Profinite.NobelingProof.continuous_swapTrue, Continuous.subtype_mk, Profinite.NobelingProof.SwapTrue, Profinite.NobelingProof.CC'₁, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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) ℤ
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 : ℤ)
⊢ 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) ℤ)

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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
⊢ 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:
dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁, LocallyConstant.sub_apply]

Premises used: Profinite.NobelingProof.Linear_CC', LocallyConstant.sub_apply, Profinite.NobelingProof.Linear_CC'₀, Profinite.NobelingProof.Linear_CC'₁
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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)) :
      ℤ)
⊢ 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:
simp only [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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))
⊢ 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:
congr 1
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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)
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
⊢ 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:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
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
⊢ (↑(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:
dsimp [CC'₀, CC'₁, ProjRestrict, Proj]

Premises used: Profinite.NobelingProof.Proj, Profinite.NobelingProof.ProjRestrict, Profinite.NobelingProof.CC'₁, Profinite.NobelingProof.CC'₀
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
apply : ord I i < o → SwapTrue o (↑x : I → Bool) i = (↑x : I → Bool) 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

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

Premises used: if_ctx_congr, Iff.rfl, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
simp : ord I i < o → ord I i = o → true = (↑x : I → Bool) i
⊢ ord I i < o → SwapTrue o (↑x : I → Bool) i = (↑x : I → Bool) i

Tactic:
simp only [SwapTrue, ite_eq_right_iff]

Premises used: Profinite.NobelingProof.SwapTrue, ite_eq_right_iff
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = (↑x : I → Bool) i

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

Premises used: False.elim, LT.lt.ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = (↑x : I → Bool) i

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

Premises used: False.elim, LT.lt.ne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
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
h : ∀ (i : I), Proj (fun (x : I) ↦ ord I x < o) x i = x i
⊢ Proj (fun (x : I) ↦ ord I x < o) x = x

Tactic:
ext i