awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
inst_1 : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
inr :
  LE.le (α := Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a \ s.erase b) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b \ s.erase a) : Colex (Finset α)) ↔
    b ≤ a
inr₂ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {b} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    b ≤ a
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase a) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase b) : Colex (Finset α)) ↔
    b ≤ a
have inr₃ : b ≤ a ↔ b ≤ a
Tactic: classical
  rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
⊢ s ≤ t ∨ t ≤ s
have inl : t ≤ t ∨ t ≤ t
Tactic: obtain rfl | hts := eq_or_ne t s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
inl : t ≤ t ∨ t ≤ t
⊢ s ≤ t ∨ t ≤ s
have inr : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
Tactic: obtain rfl | hts := eq_or_ne t s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
⊢ s ≤ t ∨ t ≤ s
have inr : ∀ (a : α)
  (ha :
    Membership.mem (γ := Finset α)
      (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
        Finset α)
      a)
  (hamax :
    ∀ (x' : α),
      Membership.mem (γ := Finset α)
          (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t)
              ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
            Finset α)
          x' →
        id x' ≤ id a),
  s ≤ t ∨ t ≤ s
Tactic: have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a_1 b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha :
  Membership.mem (γ := Finset α)
    (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
      Finset α)
    a
hamax :
  ∀ (x' : α),
    Membership.mem (γ := Finset α)
        (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
          Finset α)
        x' →
      id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s
have ha₁ : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
    a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
  Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
    a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
Tactic: simp_rw [mem_symmDiff] at ha hamax
Cleared hypotheses: ha, hamax
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a_1 b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha :
  Membership.mem (γ := Finset α)
    (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
      Finset α)
    a
hamax :
  ∀ (x' : α),
    Membership.mem (γ := Finset α)
        (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
          Finset α)
        x' →
      id x' ≤ id a
ha₁ :
  Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
      a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
⊢ s ≤ t ∨ t ≤ s
have hamax₁ : ∀ (x' : α),
  Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) x' ∧
        x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) x' ∧
        x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
    id x' ≤ id a
Tactic: simp_rw [mem_symmDiff] at ha hamax
Cleared hypotheses: ha, hamax
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
⊢ s ≤ t ∨ t ≤ s
have inl : t ≤ t ∨ t ≤ t
Tactic: classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
inl : t ≤ t ∨ t ≤ t
⊢ s ≤ t ∨ t ≤ s
have inr : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
Tactic: classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
inl : t ≤ t ∨ t ≤ t
inr inr₁ : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
⊢ s ≤ t ∨ t ≤ s
have inr₂ : ∀ (hts : t ≠ s) (a : α)
  (ha :
    Membership.mem (γ := Finset α)
      (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
        Finset α)
      a)
  (hamax :
    ∀ (x' : α),
      Membership.mem (γ := Finset α)
          (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t)
              ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
            Finset α)
          x' →
        id x' ≤ id a),
  s ≤ t ∨ t ≤ s
Tactic: classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
inl : t ≤ t ∨ t ≤ t
inr inr₁ : ∀ (hts : t ≠ s), s ≤ t ∨ t ≤ s
inr₂ :
  ∀ (hts : t ≠ s) (a : α)
    (ha :
      Membership.mem (γ := Finset α)
        (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t) ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
          Finset α)
        a)
    (hamax :
      ∀ (x' : α),
        Membership.mem (γ := Finset α)
            (symmDiff ((ofColex : (a : Colex (Finset α)) → Finset α) t)
                ((ofColex : (a : Colex (Finset α)) → Finset α) s) :
              Finset α)
            x' →
          id x' ≤ id a),
    s ≤ t ∨ t ≤ s
⊢ s ≤ t ∨ t ≤ s
have inr₃ : ∀ (hts : t ≠ s) (a : α)
  (ha :
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a ∧
        a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a ∧
        a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α))
  (hamax :
    ∀ (x' : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) x' ∧
            x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∨
          Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) x' ∧
            x' ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) →
        id x' ≤ id a),
  s ≤ t ∨ t ≤ s
Tactic: classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id
      (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
have rw : (∃ (x : α), ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Tactic: rw [← not_le, toColex_le_toColex, not_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
have refine_1 : ∀
  (h :
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)))
  (hst : s ≠ t), (s ∆ t).max' sorry ∈ t
Tactic: refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
refine_1 :
  ∀
    (h :
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)))
    (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
have refine_2 : ∀ (h : ∀ (hst : s ≠ t), (s ∆ t).max' sorry ∈ t) (a : α)
  (has :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
        Finset α)
      a)
  (hat :
    a ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)),
  ∃ (b : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        b ∧
      b ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        a ≤ b
Tactic: refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
⊢ m ∈ t
have refine_1 : ∀ (hmt : m ∉ t), False
Tactic: by_contra hmt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ False
have hms : m ∈ s
Tactic: have hms : m ∈ s := by
      simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
⊢ False
have refine_1 : ∀ (b : α)
  (hbt :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)
      b)
  (hbs :
    b ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
        Finset α))
  (hmb : m ≤ b), False
Tactic: have ⟨b, hbt, hbs, hmb⟩ := h hms hmt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)
    a
hat :
  a ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        b ∧
      b ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        a ≤ b
have hst : s ≠ t
Tactic: have hst : s ≠ t := ne_of_mem_of_not_mem' has hat
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
      Finset α)
    a
hat :
  a ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
hst : s ≠ t
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        b ∧
      b ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        a ≤ b
have refine_2 : (s ∆ t).max' sorry ∉
  ((ofColex : (a : Colex (Finset α)) → Finset α) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
    Finset α)
Tactic: refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
have rw : (∀ (hst : s ≠ t), (s ∆ t).max' sorry ∈ t) ∧
    Ne (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
  ∃ (hst : s ≠ t), (s ∆ t).max' sorry ∈ t
Tactic: rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Colex (Finset α)
⊢ s < t ↔
    ∃ (_ : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) ⋯)
have rw : (∀ (h : s ≠ t),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
        (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) sorry)) ∧
    s ≠ t ↔
  ∃ (_ : s ≠ t),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
      (max' ((ofColex : (a : Colex (Finset α)) → Finset α) s ∆ (ofColex : (a : Colex (Finset α)) → Finset α) t) sorry)
Tactic: rw [lt_iff_le_and_ne, le_iff_max'_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) ↔
    ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}
have simp : (∃ (a : α),
    Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        a ∧
      a ∉
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
            Finset α) ∧
        ∀ (b : α),
          Membership.mem (γ := Finset α)
              ((ofColex : (a : Colex (Finset α)) → Finset α)
                  ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                Finset α)
              b →
            b ∉
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                  Finset α) →
              b < a) ↔
  ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic: simp only [lt_iff_exists_forall_lt, mem_sdiff, filter_inj, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Finset α
⊢ (∃ (a : α),
      Membership.mem (γ := Finset α)
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
            Finset α)
          a ∧
        a ∉
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
              Finset α) ∧
          ∀ (b : α),
            Membership.mem (γ := Finset α)
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                  Finset α)
                b →
              b ∉
                  ((ofColex : (a : Colex (Finset α)) → Finset α)
                      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                    Finset α) →
                b < a) ↔
    ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
have refine_1 : ∀
  (h :
    ∃ (a : α),
      Membership.mem (γ := Finset α)
          ((ofColex : (a : Colex (Finset α)) → Finset α)
              ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
            Finset α)
          a ∧
        a ∉
            ((ofColex : (a : Colex (Finset α)) → Finset α)
                ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
              Finset α) ∧
          ∀ (b : α),
            Membership.mem (γ := Finset α)
                ((ofColex : (a : Colex (Finset α)) → Finset α)
                    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
                  Finset α)
                b →
              b ∉
                  ((ofColex : (a : Colex (Finset α)) → Finset α)
                      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
                    Finset α) →
                b < a),
  ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩