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
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) [a]
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ []}
hmas : (↑m : List I) ≤ []
⊢ [] ≤ [a]

Tactic:
(List.nil_lt_cons a []).le

Premises used: LT.lt.le, List.nil_lt_cons, List.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) [a]
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ []}
hmas : (↑m : List I) ≤ []
⊢ [] ≤ [a]

Tactic:
exact (List.nil_lt_cons a []).le

Premises used: LT.lt.le, List.nil_lt_cons, List.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
neg : b :: bs < a :: b :: bs
⊢ b :: bs ≤ a :: b :: bs

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
⊢ a > b ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (b :: bs)

Tactic:
rw [List.isChain_cons_cons] at ha

Premises used: List.isChain_cons_cons
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
ha₁ : a > b ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (b :: bs)
⊢ (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}

Tactic:
rw [List.isChain_cons_cons] at ha

Premises used: List.isChain_cons_cons
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
ha₁ : a > b ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (b :: bs)
hc₁ : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
⊢ (↑m : List I) ≤ b :: bs

Tactic:
rw [List.isChain_cons_cons] at ha

Premises used: List.isChain_cons_cons
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : a > b ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
⊢ b :: bs < a :: b :: bs

Tactic:
exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)

Premises used: List.Lex.rel, And.left, Iff.mp, List.lt_iff_lex_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hmas : (↑m : List I) ≤ as
neg :
  ∀ (ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) [a])
    (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ []}) (hmas : (↑m : List I) ≤ []), [] ≤ [a]
neg₁ :
  ∀ (b : I) (bs : List I) (ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs))
    (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs})
    (hmas : (↑m : List I) ≤ b :: bs), b :: bs ≤ a :: b :: bs
⊢ as ≤ a :: as

Tactic:
cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)

Premises used: le_of_lt, LT.lt.le, List.nil_lt_cons, List.isChain_cons_cons, List.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
neg :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (c.sum fun (a_1 : Products I) (b : ℤ) ↦
      e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) (-1)
      (c.sum fun (a_1 : Products I) (b : ℤ) ↦
        e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1))

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (c.sum fun (a_1 : Products I) (b : ℤ) ↦
      e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1)

Tactic:
finsuppSum_mem_span_eval _ _ ha hc

Premises used: Set.Mem, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (c.sum fun (a_1 : Products I) (b : ℤ) ↦
      e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1)

Tactic:
exact finsuppSum_mem_span_eval _ _ ha hc

Premises used: Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
induction :
  ∀ (x_1 : List I),
    List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x_1 →
      Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
        (Submodule.span ℤ
          (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
            {m : Products I | (↑m : List I) ≤ x_1}))
        (List.prod
          (List.map
            (fun (i : I) ↦
              if (↑x : I → Bool) i = true then e (π C fun (x : I) ↦ x ∈ s) i else 1 - e (π C fun (x : I) ↦ x ∈ s) i)
            x_1))
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ
        (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ l}))
      (List.prod
        (List.map
          (fun (i : I) ↦
            if (↑x : I → Bool) i = true then e (π C fun (x : I) ↦ x ∈ s) i else 1 - e (π C fun (x : I) ↦ x ∈ s) i)
          l))

Tactic:
induction l with
  | nil =>
    intro _
    apply Submodule.subset_span
    exact ⟨⟨[], List.isChain_nil⟩,⟨Or.inl rfl, rfl⟩⟩
  | cons a as ih =>
    rw [List.map_cons, List.prod_cons]
    intro ha
    specialize ih (by rw [List.isChain_cons] at ha; exact ha.2)
    rw [Finsupp.mem_span_image_iff_linearCombination] at ih
    simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih
    obtain ⟨c, hc, hc'⟩ := ih
    rw [← hc']; clear hc'
    have hmap := fun g ↦ map_finsuppSum (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)) c g
    dsimp at hmap ⊢
    split_ifs
    · rw [hmap]
      exact finsuppSum_mem_span_eval _ _ ha hc
    · noncomm_ring
      -- we use `noncomm_ring` even though this is a commutative ring, because we want a weaker
      -- normalization which preserves multiplication order (i.e. doesn't use commutativity rules)
      rw [hmap]
      apply Submodule.add_mem
      · apply Submodule.finsuppSum_mem
        intro m hm
        apply Submodule.smul_mem
        apply Submodule.subset_span
        refine ⟨m, ⟨?_, rfl⟩⟩
        simp only [Set.mem_setOf_eq]
        have hmas : m.val ≤ as :=
          hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
        refine le_trans hmas ?_
        cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)
      · apply Submodule.smul_mem
        exact finsuppSum_mem_span_eval _ _ ha hc

Premises used: Finsupp.mem_supported, List.map_cons, le_of_lt, Set.mem_setOf_eq, Finsupp.linearCombination_apply, List.isChain_cons_cons, Submodule.subset_span, Submodule.finsuppSum_mem, Finsupp.mem_span_image_iff_linearCombination, List.prod_cons, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
hC : IsClosed C
f : LocallyConstant (↑C : Type u) ℤ
obtain :
  ∀ (J : (Finset I)ᵒᵖ)
    (g :
      LocallyConstant
        (↑(((spanFunctor (C := C) ⋯).obj J).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        ℤ)
    (h :
      f =
        LocallyConstant.comap
          (TopCat.Hom.hom
            (CategoryTheory.InducedCategory.Hom.hom
              (CategoryTheory.NatTrans.app (CategoryTheory.Limits.Cone.π (spanCone (C := C) ⋯)) J)))
          g),
    ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
      f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } g
⊢ ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } g

Tactic:
obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
    (spanCone hC.isCompact) ℤ
    (spanCone_isLimit hC.isCompact) f

Premises used: Profinite.NobelingProof.spanCone, Profinite.NobelingProof.spanCone_isLimit, Profinite.exists_locallyConstant, IsClosed.isCompact
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
hC : IsClosed C
f : LocallyConstant (↑C : Type u) ℤ
J : (Finset I)ᵒᵖ
g :
  LocallyConstant
    (↑(((spanFunctor (C := C) ⋯).obj J).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    ℤ
h :
  f =
    LocallyConstant.comap
      (TopCat.Hom.hom
        (CategoryTheory.InducedCategory.Hom.hom
          (CategoryTheory.NatTrans.app (CategoryTheory.Limits.Cone.π (spanCone (C := C) ⋯)) J)))
      g
⊢ ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } g

Tactic:
⟨(Opposite.unop J), g, h⟩

Premises used: Exists.intro, Opposite.unop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
hC : IsClosed C
f : LocallyConstant (↑C : Type u) ℤ
J : (Finset I)ᵒᵖ
g :
  LocallyConstant
    (↑(((spanFunctor (C := C) ⋯).obj J).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    ℤ
h :
  f =
    LocallyConstant.comap
      (TopCat.Hom.hom
        (CategoryTheory.InducedCategory.Hom.hom
          (CategoryTheory.NatTrans.app (CategoryTheory.Limits.Cone.π (spanCone (C := C) ⋯)) J)))
      g
⊢ ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } g

Tactic:
exact ⟨(Opposite.unop J), g, h⟩
-- 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
rw :
  LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    (Submodule.span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)))

Tactic:
rw [span_iff_products]

Premises used: Profinite.NobelingProof.GoodProducts.span_iff_products
-- 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
f : LocallyConstant (↑C : Type u) ℤ
_ :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C))) f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C))) f

Tactic:
_
-- 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
f : LocallyConstant (↑C : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ f
⊢ ∃ (K : Finset I) (f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ),
    f = (πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f'

Tactic:
fin_comap_jointlySurjective C hC f

Premises used: LocallyConstant.comap, Profinite.NobelingProof.fin_comap_jointlySurjective
-- 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
f : LocallyConstant (↑C : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ f
obtain :
  ∀ (K : Finset I) (f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ),
    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) ℤ) →
      Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
        (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
        ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
          LocallyConstant (↑C : Type u) ℤ)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C))) f

Tactic:
obtain ⟨K, f', rfl⟩ : ∃ K f', f = πJ C K f' := fin_comap_jointlySurjective C hC f

Premises used: Profinite.NobelingProof.fin_comap_jointlySurjective, rfl
-- 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) ℤ)
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
Submodule.span_mono ?_ <| Submodule.apply_mem_span_image_of_mem_span (πJ C K) <|
    spanFin C K (Submodule.mem_top : f' ∈ ⊤)

Premises used: Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.πJ, Submodule.apply_mem_span_image_of_mem_span, Submodule.span_mono, Submodule.mem_top
-- 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) ℤ)
refine :
  (⇑(πJ C K) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
      Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ x ∈ K) l })
        (eval (π C fun (x : I) ↦ x ∈ K)) ⊆
    Set.range (ι := Products I) (Products.eval C)
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
refine Submodule.span_mono ?_ <| Submodule.apply_mem_span_image_of_mem_span (πJ C K) <|
    spanFin C K (Submodule.mem_top : f' ∈ ⊤)

Premises used: Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.πJ, Submodule.apply_mem_span_image_of_mem_span, Submodule.span_mono, Submodule.mem_top