-- Mathlib/Combinatorics/Colex.lean
private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toColex u)
    (has : a ∈ s) (hat : a ∉ t) : ∃ b, b ∈ u ∧ b ∉ s ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1

Result:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s'
hbmax : ∀ x ∈ s', ¬b < x
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

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

Result:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
let s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}

Result:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd

Result:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
had : a ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
had : a ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
refine ⟨d, hdu, fun hds ↦ ?_, had⟩

Result:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
had : a ≤ d
hds : d ∈ s
⊢ False

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨b, hb, hbmax⟩ := exists_maximal s' ⟨a, by simp [s', has, hat]⟩

Result:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s'
hbmax : ∀ x ∈ s', ¬b < x
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∈ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

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

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
by_cases hcu : c ∈ u

Result:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∈ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu

Result:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b