awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
case₁ :
  HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
case₂ :
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
case₃ : (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) = 2 / ε - 1
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have case₄ : HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) ≤
  (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: case cardZ =>
    calc
          (#Z : ℝ)
      _ = #(H : Set G).toFinset * #Z / #(H : Set G).toFinset          := by field
      _ = #(Set.toFinset H * Z) / #(H : Set G).toFinset               := by
        simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]
      _ = #(Set.toFinset H * S) / #(H : Set G).toFinset               := by
        congr 3; simpa using congr(($hHZS).toFinset)
      _ ≤ (2 / ε - 1) * #(H : Set G).toFinset / #(H : Set G).toFinset := ?_
      _ = 2 / ε - 1                                                   := by field
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
case₁ :
  HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
case₂ :
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
case₃ : (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) = 2 / ε - 1
case₄ :
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) ≤
    (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have hab : (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: case cardZ =>
    calc
          (#Z : ℝ)
      _ = #(H : Set G).toFinset * #Z / #(H : Set G).toFinset          := by field
      _ = #(Set.toFinset H * Z) / #(H : Set G).toFinset               := by
        simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]
      _ = #(Set.toFinset H * S) / #(H : Set G).toFinset               := by
        congr 3; simpa using congr(($hHZS).toFinset)
      _ ≤ (2 / ε - 1) * #(H : Set G).toFinset / #(H : Set G).toFinset := ?_
      _ = 2 / ε - 1                                                   := by field
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have have : ∀ (b : α) (hb : b ∈ s') (hbmax : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ s') y → b ≤ y → y ≤ b), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: have ⟨b, hb, hbmax⟩ := s'.exists_maximal ⟨a, by simp [s', has, hat]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : (fun (x : α) ↦ x ∈ s') b
hbmax : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ s') y → b ≤ y → y ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have hb₁ : b ∈ s ∧ b ∉ t ∧ a ≤ b
Tactic: simp only [s', mem_filter, and_imp] at hb hbmax
Cleared hypotheses: hb, hbmax
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : (fun (x : α) ↦ x ∈ s') b
hbmax : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ s') y → b ≤ y → y ≤ b
hb₁ : b ∈ s ∧ b ∉ t ∧ a ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have hbmax₁ : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
Tactic: simp only [s', mem_filter, and_imp] at hb hbmax
Cleared hypotheses: hb, hbmax
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
have have : ∀ (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
Tactic: have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
have pos : ∀ (hcu : c ∈ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: by_cases hcu : c ∈ u
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
pos : ∀ (hcu : c ∈ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have neg : ∀ (hcu : c ∉ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: by_cases hcu : c ∈ u
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
have neg : ∀ (d : α)
  (hdu :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α)) :
        Finset α)
      d)
  (hdt :
    d ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α))
  (hcd : c ≤ d), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu
-- Lean 4 proof step from Mathlib.Combinatorics.Colex (hypothesis)
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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
d : α
hdu :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α)) :
      Finset α)
    d
hdt :
  d ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
hcd : c ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have had : a ≤ d
Tactic: have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd
-- 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
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
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
d : α
hdu :
  Membership.mem (γ := Finset α)
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α)) :
      Finset α)
    d
hdt :
  d ∉
    ((ofColex : (a : Colex (Finset α)) → Finset α)
        ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
      Finset α)
hcd : c ≤ d
had : a ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have neg : ∀ (hds : d ∈ s), b < d
Tactic: refine ⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩
-- 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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have 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
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 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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have 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
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 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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have 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
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 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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have 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
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