awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
⊢ (↑(#((↑H : Set G).toFinset * S)) : ℝ) =
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + ((↑(#((↑H : Set G).toFinset * S)) : ℝ) - K * (↑(#(↑H : Set G).toFinset) : ℝ))

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + ((↑(#((↑H : Set G).toFinset * S)) : ℝ) - K * (↑(#(↑H : Set G).toFinset) : ℝ)) =
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + ex (↑H : Set G).toFinset

Tactic:
rfl

Premises used: _private.0.Finset.expansion, rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
grw :
  K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#S) : ℝ) ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + ex (↑H : Set G).toFinset ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)

Tactic:
grw [calc₁]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
bc : 0 ≤ 1 - ε / 2
bc₁ : S ⊆ (↑H : Set G).toFinset * S
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#S) : ℝ) ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ε / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ε / 2 < 0 → 2 / 2 = 1
linarith₄ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₆ : 1 - ε / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₇ : 1 - ε / 2 < 0 → -1 + (ε - 1) + (HMul.hMul (α := ℝ) 2 1 - 1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ 1 - ε / 2

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
⊢ S ⊆ (↑H : Set G).toFinset * S

Tactic:
simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]

Premises used: Finset.subset_mul_right, Subgroup.one_mem, SetLike.mem_coe, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
H₁ :
  (↑(#((↑H : Set G).toFinset * S)) : ℝ) =
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + ((↑(#((↑H : Set G).toFinset * S)) : ℝ) - K * (↑(#(↑H : Set G).toFinset) : ℝ))
H₂ :
  K * (↑(#(↑H : Set G).toFinset) : ℝ) + ex (↑H : Set G).toFinset ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
⊢ (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤
    (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) + K * (↑(#((↑H : Set G).toFinset * S)) : ℝ)

Tactic:
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]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Set.toFinset, Nat.cast, SetLike.coe, Finset.card, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hA₀ : A.Nonempty
hA₁ : (↑(#(A * A)) : ℝ) ≤ (2 - ε) * (↑(#A) : ℝ)
⊢ #A ≤ #A

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Colex
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}
⊢ a ∈ s'

Tactic:
simp [s', has, hat]
-- Module: Mathlib.Combinatorics.Colex
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}
have : ∀ (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

Tactic:
have ⟨b, hb, hbmax⟩ := s'.exists_maximal ⟨a, by simp [s', has, hat]⟩
-- Module: Mathlib.Combinatorics.Colex
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 ∈ s ∧ b ∉ t ∧ a ≤ b

Tactic:
simp only [s', mem_filter, and_imp] at hb hbmax

Premises used: and_imp, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Colex
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
⊢ ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b

Tactic:
simp only [s', mem_filter, and_imp] at hb hbmax

Premises used: and_imp, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Colex
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
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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1
-- Module: Mathlib.Combinatorics.Colex
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
neg : ∀ (hcu : c ∉ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
by_cases hcu : c ∈ u
-- Module: Mathlib.Combinatorics.Colex
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

Tactic:
⟨c, hcu, hcs, hb.2.2.trans hbc⟩

Premises used: And.right, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Combinatorics.Colex
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

Tactic:
exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩
-- Module: Mathlib.Combinatorics.Colex
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
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
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu
-- Module: Mathlib.Combinatorics.Colex
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
⊢ a ≤ d

Tactic:
have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd
-- Module: Mathlib.Combinatorics.Colex
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

Tactic:
⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩

Premises used: Iff.mpr, And.intro, Exists.intro, not_lt_iff_le_imp_ge
-- Module: Mathlib.Combinatorics.Colex
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
neg : ∀ (hds : d ∈ s), b < d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
refine ⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩
-- Module: Mathlib.Combinatorics.Colex
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
hds : d ∈ s
⊢ b < d

Tactic:
hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Colex
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
hds : d ∈ s
⊢ b < d

Tactic:
exact hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt

Premises used: ne_of_mem_of_not_mem, LE.le.lt_of_ne, LE.le.trans_lt