Theorem: Finset.UV.toColex_compress_lt_toColex (LeanCamCombi/KruskalKatona.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
Tactic:
rw [compress, ite_ne_right_iff] at hA
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
Tactic:
rw [compress, if_pos hA.1, lt_iff_exists_forall_lt_mem_iff_mem]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Tactic:
refine ⟨_, hA.1.2 $ max'_mem _ hV, not_mem_sdiff_of_mem_right $ max'_mem _ _, fun a ha ↦ ?_⟩
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
have : a ∉ V := fun H ↦ ha.not_le (le_max' _ _ H)
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
have : a ∉ U := fun H ↦ ha.not_lt ((le_max' _ _ H).trans_lt h)
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this✝ : a ∉ V
this : a ∉ U
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this✝ : a ∉ V
this : a ∉ U
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
simp [‹a ∉ U›, ‹a ∉ V›]
State after:
no goals