awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
cards : card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t
le :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
p :
  Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
h h₁ h₂ h₃ : 𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)) ∈ 𝒜
⊢ t ∈ 𝒜

Tactic:
rwa [toColex_inj.1 p]

Premises used: toColex_inj, Iff.mp
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
cards : card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t
le :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
p :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
⊢ t ∈ 𝒜

Tactic:
h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

Premises used: Eq.rec, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs :
  Membership.mem (γ := Set (Colex (Finset α)))
    ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
    (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
t : Finset α
cards : card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t
le :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
p :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) :
      Colex (Finset α))
⊢ t ∈ 𝒜

Tactic:
exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

Premises used: Eq.rec, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
⊢ IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s

Tactic:
⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩

Premises used: Finset.Colex.IsInitSeg.exists_initSeg, And.right, And.left, Iff.intro
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
refine : (∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty
⊢ IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Fintype α
s : Finset α
⊢ IsInitSeg (initSeg s) #s ∧ (initSeg s).Nonempty

Tactic:
⟨isInitSeg_initSeg, initSeg_nonempty⟩

Premises used: Finset.Colex.initSeg_nonempty, And.intro, Finset.Colex.isInitSeg_initSeg
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Fintype α
s : Finset α
⊢ IsInitSeg (initSeg s) #s ∧ (initSeg s).Nonempty

Tactic:
exact ⟨isInitSeg_initSeg, initSeg_nonempty⟩
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : s < t
⊢ ∃ (a : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a ∧
      a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) ∧
        ∀ (b : ℕ),
          Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
            b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a

Tactic:
rw [Colex.lt_iff_exists_forall_lt] at hst

Premises used: Finset.Colex.lt_iff_exists_forall_lt
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst :
  ∃ (a : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a ∧
      a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) ∧
        ∀ (b : ℕ),
          Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
            b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a
obtain :
  ∀ (a : ℕ) (hat : Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a)
    (has : a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ))
    (ha :
      ∀ (b : ℕ),
        Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
          b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a),
    LT.lt (α := ℕ) ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) s)
      ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) t)
⊢ LT.lt (α := ℕ) ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) s)
    ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) t)

Tactic:
obtain ⟨a, hat, has, ha⟩ := hst
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a
has : a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ)
ha :
  ∀ (b : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
      b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a
rw :
  LT.lt (α := ℕ)
    (∑ i ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t, n ^ i)
    (∑ i ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ i)
⊢ LT.lt (α := ℕ) ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) s)
    ((fun (s : Colex (Finset ℕ)) ↦ (∑ k ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ k : ℕ)) t)

Tactic:
rw [← sum_sdiff_lt_sum_sdiff]

Premises used: Finset.sum_sdiff_lt_sum_sdiff
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a
has : a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ)
ha :
  ∀ (b : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
      b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a
⊢ ∀ (k : ℕ),
    Membership.mem (γ := Finset ℕ)
        ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ)
        k →
      k < a

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a
has : a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ)
ha :
  ∀ (b : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
      b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a
x : ℕ
h :
  Membership.mem (γ := Finset ℕ)
    ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) x
⊢ 0 ≤ n ^ x

Tactic:
lia
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) a
has : a ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ)
ha :
  ∀ (b : ℕ),
    Membership.mem (γ := Finset ℕ) ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ) b →
      b ∉ ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t : Finset ℕ) → b < a
⊢ LT.lt (α := ℕ)
    (∑ i ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t, n ^ i)
    (∑ i ∈ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) t \ (ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s, n ^ i)

Tactic:
exact (Nat.geomSum_lt hn <| by simpa).trans_le <| single_le_sum (fun _ _ ↦ by lia) <|
    mem_sdiff.2 ⟨hat, has⟩

Premises used: Iff.mpr, Nat.geomSum_lt, Finset.mem_sdiff, LT.lt.trans_le, And.intro, Finset.single_le_sum
-- Module: Mathlib.Combinatorics.Colex
Goal:
s t : Finset ℕ
n : ℕ
hn : 2 ≤ n
⊢ LE.le (α := ℕ) (∑ k ∈ s, n ^ k) (∑ k ∈ t, n ^ k) ↔
    LE.le (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) s : Colex (Finset ℕ))
      ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) t : Colex (Finset ℕ))

Tactic:
(geomSum_ofColex_strictMono hn).le_iff_le

Premises used: Set.Mem, setOf, Finset.geomSum_ofColex_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Combinatorics.Colex
Goal:
s t : Finset ℕ
n : ℕ
hn : 2 ≤ n
⊢ LT.lt (α := ℕ) (∑ i ∈ s, n ^ i) (∑ i ∈ t, n ^ i) ↔
    LT.lt (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) s : Colex (Finset ℕ))
      ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) t : Colex (Finset ℕ))

Tactic:
(geomSum_ofColex_strictMono hn).lt_iff_lt

Premises used: Set.Mem, setOf, StrictMono.lt_iff_lt, Finset.geomSum_ofColex_strictMono
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
a₁ : Finset ℕ
_ :
  ∀ ⦃a₂ : Finset ℕ⦄,
    Eq (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : Finset ℕ⦄,
    Eq (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
hn : 2 ≤ n
a₁ a₂ : Finset ℕ
h : Eq (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂)
rwa :
  ∀
    (h :
      LE.le (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂) ∧
        LE.le (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂)
          ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁)),
    a₁ = a₂
rwa₁ :
  ∀
    (h :
      LE.le (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₁ : Colex (Finset ℕ))
          ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₂ : Colex (Finset ℕ)) ∧
        LE.le (α := ℕ) ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₂)
          ((fun (s : Finset ℕ) ↦ (∑ i ∈ s, n ^ i : ℕ)) a₁)),
    a₁ = a₂
rwa₂ :
  ∀
    (h :
      LE.le (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₁ : Colex (Finset ℕ))
          ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₂ : Colex (Finset ℕ)) ∧
        LE.le (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₂ : Colex (Finset ℕ))
          ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₁ : Colex (Finset ℕ))),
    a₁ = a₂
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (h :
      Eq (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₁ : Colex (Finset ℕ))
        ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₂ : Colex (Finset ℕ))),
    a₁ = a₂
⊢ a₁ = a₂

Tactic:
rwa [le_antisymm_iff, geomSum_le_geomSum_iff_toColex_le_toColex hn,
    geomSum_le_geomSum_iff_toColex_le_toColex hn, ← le_antisymm_iff] at h

Premises used: Finset.geomSum_le_geomSum_iff_toColex_le_toColex, le_antisymm_iff
-- Module: Mathlib.Combinatorics.Colex
Goal:
s : Finset ℕ
n a : ℕ
hn : 2 ≤ n
hi : a ∈ s
⊢ ∀ i ∈ s, 0 ≤ n ^ i

Tactic:
simp
-- Module: Mathlib.Combinatorics.Colex
Goal:
s : Finset ℕ
⊢ (Nat.bitIndices (∑ i ∈ s, HPow.hPow (α := ℕ) 2 i)).toFinset = s

Tactic:
simp [← (geomSum_injective rfl.le).eq_iff, List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Premises used: Nat.bitIndices_sorted, List.SortedLT.nodup, Function.Injective.eq_iff, List.sum_toFinset, Eq.le, Finset.geomSum_injective, rfl
-- Module: Mathlib.Combinatorics.Colex
Goal:
n : ℕ
⊢ ∑ i ∈ n.bitIndices.toFinset, HPow.hPow (α := ℕ) 2 i = n

Tactic:
simp [List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Premises used: Nat.bitIndices_sorted, List.SortedLT.nodup, List.sum_toFinset
-- Module: Mathlib.Combinatorics.Colex
Goal:
α : Type u_1
β : Type u_2
s t : Finset ℕ
n : ℕ
⊢ ∀ {a b : ℕ},
    LE.le (α := Colex (Finset ℕ))
        (({
                toFun := fun (n : ℕ) ↦
                  (toColex : (a : Finset ℕ) → Colex (Finset ℕ)) ((equivBitIndices : (a : ℕ) → Finset ℕ) n : Finset ℕ),
                invFun := fun (s : Colex (Finset ℕ)) ↦
                  (equivBitIndices.symm : (a : Finset ℕ) → ℕ)
                    ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : ℕ) → Colex (Finset ℕ))
            a :
          Colex (Finset ℕ))
        (({
                toFun := fun (n : ℕ) ↦
                  (toColex : (a : Finset ℕ) → Colex (Finset ℕ)) ((equivBitIndices : (a : ℕ) → Finset ℕ) n : Finset ℕ),
                invFun := fun (s : Colex (Finset ℕ)) ↦
                  (equivBitIndices.symm : (a : Finset ℕ) → ℕ)
                    ((ofColex : (a : Colex (Finset ℕ)) → Finset ℕ) s : Finset ℕ),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : ℕ) → Colex (Finset ℕ))
            b :
          Colex (Finset ℕ)) ↔
      a ≤ b

Tactic:
simp [← (Finset.geomSum_le_geomSum_iff_toColex_le_toColex rfl.le)]

Premises used: Finset.geomSum_le_geomSum_iff_toColex_le_toColex, Eq.le, rfl
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
⊢ ∀ (a : α), DiscreteTopology.{u_2} (β a)

Tactic:
have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
s : Finset α
⊢ s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s

Tactic:
simp [e]
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
⊢ ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s

Tactic:
have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
s : Finset α
rw :
  IsClosed (X := (a : α) → β a)
    (s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)})
⊢ IsClosed (e s)

Tactic:
rw [← this]
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
s : Finset α
⊢ Continuous (X := (a : α) → β a) (s.restrict (π := β))

Tactic:
fun_prop
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
s : Finset α
⊢ IsClosed (X := (a : α) → β a)
    (s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)})

Tactic:
exact (isClosed_discrete _).preimage (by fun_prop)

Premises used: isClosed_discrete, IsClosed.preimage
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
⊢ ∀ (s : Finset α), IsClosed (e s)

Tactic:
have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
⊢ Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)

Tactic:
⟨g (B.biUnion id), ?_⟩

Premises used: id, Finset.biUnion, Set.Nonempty, Exists.intro
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
refine : Membership.mem (γ := Set ((a : α) → β a)) (⋂ i ∈ B, e i) (g (B.biUnion id))
⊢ Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)

Tactic:
refine ⟨g (B.biUnion id), ?_⟩
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
simp : ∀ (i : Finset α) (i_1 : i ∈ B), ∃ (t : Finset α), i ⊆ t ∧ ∀ x ∈ i, g (B.biUnion id) x = g t x
⊢ Membership.mem (γ := Set ((a : α) → β a)) (⋂ i ∈ B, e i) (g (B.biUnion id))

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq, e]

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
i : Finset α
hi : i ∈ B
⊢ ∀ x ∈ i, g (B.biUnion id) x = g (B.biUnion id) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
i : Finset α
hi : i ∈ B
⊢ ∃ (t : Finset α), i ⊆ t ∧ ∀ x ∈ i, g (B.biUnion id) x = g t x

Tactic:
exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
⊢ ∀ (B : Finset (Finset α)), Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)

Tactic:
have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩