awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
htu :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α))
has : a ∈ s
hat : a ∉ t
let let₁ let₂ : ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₃ :
  let s' := {b ∈ s | b ∉ t ∧ a ≤ b};
  ∀ (b : α) (hb : b ∈ s') (hbmax : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ s') y → b ≤ y → y ≤ b), ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₄ :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b),
    ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₅ :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hcs :
      c ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hbc : b ≤ c), ∃ b ∈ u, b ∉ s ∧ a ≤ b
pos :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hcs :
      c ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hbc : b ≤ c) (hcu : c ∈ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have neg : ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
  (hct :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)
      c)
  (hcs :
    c ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
        Finset α))
  (hbc : b ≤ c) (hcu : c ∉ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: classical
  let s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
  have ⟨b, hb, hbmax⟩ := s'.exists_maximal ⟨a, by simp [s', has, hat]⟩
  simp only [s', mem_filter, and_imp] at hb hbmax
  have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1
  by_cases hcu : c ∈ u
  · exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩
  have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu
  have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd
  refine ⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩
  exact hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
⊢ a ∈ t
have by_contra : ∀ (hat : a ∉ t), False
Tactic: by_contra hat
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
a : α
has : a ∈ s
hat : a ∉ t
⊢ False
have have : ∀ (_b : α) (hb₁ : _b ∈ s) (hb₂ : _b ∉ s), a ≤ _b → False
Tactic: have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have pos : ∀ (hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: by_cases hat : a ∈ ofColex t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
pos :
  ∀ (hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have neg : ∀ (hat : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: by_cases hat : a ∈ ofColex t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have pos : ∀ (b : α) (hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b)
  (hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)) (hab : a ≤ b),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: have ⟨b, hbu, hbt, hab⟩ := htu hat hau
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have pos : ∀ (hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: by_cases hbs : b ∈ ofColex s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
pos :
  ∀ (hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b),
    ∃ (b : α),
      Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
        b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have neg : ∀ (hbs : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α)),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: by_cases hbs : b ∈ ofColex s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s_1 t_1 u_1 : Finset α
a_1 b_1 : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) a
hau : a ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α)
hat : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α) a
b : α
hbu : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b
hbt : b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) t : Finset α)
hab : a ≤ b
hbs : Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) b
⊢ ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
have pos : ∀ (c : α) (hcu : c ∈ u) (hcs : c ∉ s) (hbc : b ≤ c),
  ∃ (b : α),
    Membership.mem (γ := Finset α) ((ofColex : (a : Colex (Finset α)) → Finset α) u : Finset α) b ∧
      b ∉ ((ofColex : (a : Colex (Finset α)) → Finset α) s : Finset α) ∧ a ≤ b
Tactic: have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
⊢ b ≤ a
have pos : b ∈ t → b ≤ a
Tactic: by_cases b ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
pos : b ∈ t → b ≤ a
⊢ b ≤ a
have neg : b ∉ t → b ≤ a
Tactic: by_cases b ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h : b ∉ t
⊢ b ≤ a
have neg : ∀ (c : α)
  (hct :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)
      c)
  (hbc : b ≤ c), b ≤ a
Tactic: obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
⊢ b < a
have pos : b ∈ t → b < a
Tactic: by_cases b ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
pos : b ∈ t → b < a
⊢ b < a
have neg : b ∉ t → b < a
Tactic: by_cases b ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h : b ∉ t
⊢ b < a
have neg : ∀ (c : α)
  (hct :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)
      c)
  (hbc : b ≤ c), b < a
Tactic: obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
have simp : (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
Tactic: simp only [toColex_le_toColex, mem_singleton, exists_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
have refine : ∀ b ∈ s, ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
Tactic: refine forall₂_congr fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
h : b ∈ s
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
have inl : ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)
Tactic: obtain rfl | hba := eq_or_ne b a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a b : α
h : b ∈ s
inl : ¬b = b → b ∉ s ∧ b ≤ b ↔ b ≤ b ∧ (b ∈ s → b = b)
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
have inr : ∀ (hba : b ≠ a), ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
Tactic: obtain rfl | hba := eq_or_ne b a
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α)) ↔
    ∀ b ∈ s, b < a
have rw : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
Tactic: rw [lt_iff_le_and_ne, toColex_le_singleton, ne_eq, toColex_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
have refine_1 : ∀ (h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}) (b : α) (hb : b ∈ s), b ≠ a
Tactic: refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
refine_1 : ∀ (h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}) (b : α) (hb : b ∈ s), b ≠ a
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
have refine_2 : ∀ (h : ∀ b ∈ s, b < a), ¬s = {a}
Tactic: refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) {a} : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) ↔
    ∃ x ∈ s, a ≤ x
have simp : (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
Tactic: simp [toColex_le_toColex]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
have pos : a ∈ s → ((a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Finset α
a : α
pos : a ∈ s → ((a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x)
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
have neg : a ∉ s → ((a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
have simp_rw : (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
Tactic: simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
have simp_rw₁ : (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
Tactic: simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₁ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
have simp_rw₂ : (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ (b : α), (b ∈ t \ u ∧ b ∉ s \ u) ∧ a ≤ b) ↔
  ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ (b : α), (b ∈ t ∧ b ∉ s) ∧ a ≤ b
Tactic: simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₁ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₂ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ (b : α), (b ∈ t \ u ∧ b ∉ s \ u) ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ (b : α), (b ∈ t ∧ b ∉ s) ∧ a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
have simp_rw₃ : (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ (t \ u) \ (s \ u), a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
Tactic: simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
inst_1 : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
simp_rw :
  (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₁ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
simp_rw₂ :
  (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ (b : α), (b ∈ t \ u ∧ b ∉ s \ u) ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ (b : α), (b ∈ t ∧ b ∉ s) ∧ a ≤ b
simp_rw₃ :
  (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ (t \ u) \ (s \ u), a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (s \ u) : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (t \ u) : Colex (Finset α)) ↔
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
have simp_rw₄ : (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ t \ s, a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
Tactic: simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
    sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]