awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
⊢ IsInitSeg (initSeg s) #s
have refine : ∀ (t₁ t₂ : Finset α) (ht₁ : t₁ ∈ initSeg s)
  (ht₂ :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
      #t₂ = #s),
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
Tactic: refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α)) ∧
    #t₂ = #s
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₂ : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
have ht₃ : #s = #t₁ ∧
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t₁ : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
Tactic: rw [mem_initSeg] at ht₁
Cleared hypotheses: ht₁, ht₂
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
⊢ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s
have hs : Membership.mem (γ := Set (Colex (Finset α))) ((⇑ofColex : (a : Colex (Finset α)) → Finset α) ⁻¹' (↑𝒜 : Set (Finset α)))
  (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
Tactic: have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex
    (fun a ha ↦ by simpa using ha)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α)))
⊢ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s
have refine : 𝒜 = initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
Tactic: refine ⟨_, h𝒜.1 hs, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α)))
⊢ 𝒜 = initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))
have h : ∀ (t : Finset α),
  t ∈ 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α
⊢ t ∈ 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (initSeg (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)))) t
have h : t ∈ 𝒜 ↔
  card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
    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 α))
Tactic: rw [mem_initSeg]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α
⊢ t ∈ 𝒜 ↔
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      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 α))
have h : ∀ (p : t ∈ 𝒜),
  card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
    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 α))
Tactic: refine ⟨fun p ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α
h :
  ∀ (p : t ∈ 𝒜),
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      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 α))
⊢ t ∈ 𝒜 ↔
    card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
      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 α))
have h₁ : card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
    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 α)) →
  t ∈ 𝒜
Tactic: refine ⟨fun p ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α
p : t ∈ 𝒜
⊢ card (α := α) (𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α))) = #t ∧
    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 α))
have h : r = r ∧
  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 α))
Tactic: rw [h𝒜.1 p, h𝒜.1 hs]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
⊢ t ∈ 𝒜
have h : ∀
  (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 α))),
  t ∈ 𝒜
Tactic: obtain p | p := le.eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
h :
  ∀
    (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 α))),
    t ∈ 𝒜
⊢ t ∈ 𝒜
have h₁ : ∀
  (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: obtain p | p := le.eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 α))
⊢ t ∈ 𝒜
have h : 𝒜.sup' h𝒜₀ (⇑toColex : (a : Finset α) → Colex (Finset α)) ∈ 𝒜
Tactic: rwa [toColex_inj.1 p]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Fintype α
⊢ IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s
have refine : (∃ (s : Finset α), #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty
Tactic: refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : s < 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)
have 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
Tactic: rw [Colex.lt_iff_exists_forall_lt] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨a, hat, has, ha⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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 (α := ℕ) ((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)
have 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)
Tactic: rw [← sum_sdiff_lt_sum_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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₂)
⊢ a₁ = a₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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₂
⊢ a₁ = a₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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₂
⊢ a₁ = a₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
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₂
⊢ a₁ = a₂
have rwa₃ : ∀
  (h :
    Eq (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₁ : Colex (Finset ℕ))
      ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) a₂ : Colex (Finset ℕ))),
  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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
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 : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
Tactic: have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
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}
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
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)
have rw : IsClosed (X := (a : α) → β a)
  (s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)})
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
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
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have he' : ∀ (s : Finset α), IsClosed (e s)
Tactic: have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
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)
have refine : Membership.mem (γ := Set ((a : α) → β a)) (⋂ i ∈ B, e i) (g (B.biUnion id))
Tactic: refine ⟨g (B.biUnion id), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
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 α)
⊢ Membership.mem (γ := Set ((a : α) → β a)) (⋂ i ∈ B, e i) (g (B.biUnion id))
have simp : ∀ (i : Finset α) (i_1 : i ∈ B), ∃ (t : Finset α), i ⊆ t ∧ ∀ x ∈ i, g (B.biUnion id) x = g t x
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq, e]