awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
_ne : Nonempty α
s : Finset ι
⊢ CanLift (↥s → α) (ι → α) (fun (f : ι → α) (i : ↥s) ↦ f (↑i : ι)) fun (x : ↥s → α) ↦ True

Tactic:
PiFinsetCoe.canLift ι (fun _ => α) s

Premises used: Finset.PiFinsetCoe.canLift
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
⊢ (↑(↑s : Set α) : Type u_1) = ↥s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s ≤ t → s ⊆ t

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Std.Refl fun (x1 x2 : Finset α) ↦ x1 ⊆ x2

Tactic:
inferInstanceAs <| Std.Refl (· ≤ ·)

Premises used: _private.0.Finset.instReflSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsTrans.{u_1 + 1} (Finset α) fun (x1 x2 : Finset α) ↦ x1 ⊆ x2

Tactic:
inferInstanceAs <| IsTrans (Finset α) (· ≤ ·)

Premises used: _private.0.Finset.instIsTransSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Std.Antisymm fun (x1 x2 : Finset α) ↦ x1 ⊆ x2

Tactic:
inferInstanceAs <| Std.Antisymm (· ≤ ·)

Premises used: _private.0.Finset.instAntisymmSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Std.Irrefl fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
inferInstanceAs <| Std.Irrefl (· < ·)

Premises used: _private.0.Finset.instIrreflSSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsTrans.{u_1 + 1} (Finset α) fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
inferInstanceAs <| IsTrans (Finset α) (· < ·)

Premises used: _private.0.Finset.instIsTransSSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Std.Asymm fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
inferInstanceAs <| Std.Asymm (· < ·)

Premises used: _private.0.Finset.instAsymmSSubset._proof_1
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsNonstrictStrictOrder.{u_1} (Finset α) (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
⟨fun _ _ => Iff.rfl⟩

Premises used: Iff.rfl, IsNonstrictStrictOrder.mk
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊆ t ↔ s.val ⊆ t.val

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
⊢ s ⊆ s

Tactic:
Multiset.Subset.refl _

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.Subset.refl, Multiset.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
⊢ s ⊆ s

Tactic:
Subset.refl _

Premises used: Finset.Subset.refl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
h : s = t
⊢ s ⊆ t

Tactic:
h ▸ Subset.refl _

Premises used: Finset.Subset.refl, Eq.rec
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ s₃ : Finset α
⊢ s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃

Tactic:
Multiset.Subset.trans

Premises used: Set.Mem, setOf, Multiset.Subset.trans, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ s₃ : Finset α
⊢ s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃

Tactic:
fun h' h =>
  Subset.trans h h'

Premises used: Finset.Subset.trans
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
a : α
⊢ s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

Tactic:
Multiset.mem_of_subset

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_of_subset, Multiset.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
h : s ⊆ t
a : α
⊢ ¬a ∈ t → ¬a ∈ s

Tactic:
mt <| @h _

Premises used: mt
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
H₁ : s₁ ⊆ s₂
H₂ : s₂ ⊆ s₁
⊢ s₁ = s₂

Tactic:
ext fun a => ⟨@H₁ a, @H₂ a⟩

Premises used: Finset.ext, Iff.intro
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
simp only [subset_iff, not_imp_not]

Premises used: Finset.subset_iff, not_imp_not
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ (↑s₁ : Set α) ⊆ (↑s₂ : Set α) ↔ s₁ ⊆ s₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂

Tactic:
le_iff_subset s₁.2

Premises used: Multiset.le_iff_subset, Set.Mem, setOf, Finset.nodup, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁

Tactic:
le_antisymm_iff

Premises used: le_antisymm_iff
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ ¬s ⊆ t ↔ ∃ (x : α), x ∈ s ∧ ¬x ∈ t

Tactic:
simp only [← coe_subset, Set.not_subset, mem_coe]

Premises used: Set.not_subset, Finset.mem_coe, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α → Prop) (fun (x1 x2 : Finset α) ↦ x1 ≤ x2) fun (x1 x2 : Finset α) ↦ x1 ⊆ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α → Prop) (fun (x1 x2 : Finset α) ↦ x1 < x2) fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
rfl

Premises used: Set.Subset, rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁ ≤ s₂ ↔ s₁ ⊆ s₂

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁ < s₂ ↔ s₁ ⊂ s₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ (↑s₁ : Set α) ⊂ (↑s₂ : Set α) ↔ s₁ ⊂ s₂

Tactic:
simp
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁.val < s₂.val ↔ s₁ ⊂ s₂

Tactic:
and_congr val_le_iff <| not_congr val_le_iff

Premises used: not_congr, Finset.val_le_iff, and_congr
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
⊢ StrictMono.{u_1, u_1} (α := Finset α) val

Tactic:
fun _ _ ↦ val_lt_iff.2

Premises used: Iff.mpr, Finset.val_lt_iff, StrictMono, Set.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊂ t ↔ s ⊆ t ∧ s ≠ t

Tactic:
@lt_iff_le_and_ne _ _ s t

Premises used: lt_iff_le_and_ne, Set.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ s₁ ⊂ s₂ ↔ ∃ (x : α), x ∈ s₂ ∧ ¬x ∈ s₁

Tactic:
Set.ssubset_iff_of_subset h

Premises used: Set.Subset, Set.ssubset_iff_of_subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ s₃ : Finset α
hs₁s₂ : s₁ ⊂ s₂
hs₂s₃ : s₂ ⊆ s₃
⊢ s₁ ⊂ s₃

Tactic:
Set.ssubset_of_ssubset_of_subset hs₁s₂ hs₂s₃

Premises used: Set.Subset, Set.ssubset_of_ssubset_of_subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ s₃ : Finset α
hs₁s₂ : s₁ ⊆ s₂
hs₂s₃ : s₂ ⊂ s₃
⊢ s₁ ⊂ s₃

Tactic:
Set.ssubset_of_subset_of_ssubset hs₁s₂ hs₂s₃

Premises used: Set.Subset, Set.ssubset_of_subset_of_ssubset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
h : s₁ ⊂ s₂
⊢ ∃ (x : α), x ∈ s₂ ∧ ¬x ∈ s₁

Tactic:
Set.exists_of_ssubset h

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsWellFounded.{u_1} (Finset α) fun (x1 x2 : Finset α) ↦ x1 ⊂ x2

Tactic:
Subrelation.isWellFounded (InvImage _ _) val_lt_iff.2

Premises used: Iff.mpr, Finset.val_lt_iff, InvImage, Subrelation.isWellFounded
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ WellFoundedLT.{u_1} (Finset α)

Tactic:
Finset.isWellFounded_ssubset

Premises used: Finset.isWellFounded_ssubset, Set.Subset
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
⊢ Eq (α := (a : Finset α) → Set α) (⇑coeEmb : (a : Finset α) → Set α) SetLike.coe

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
p : α → Prop
_hp : (a : α) → Decidable (p a)
⊢ (∃ (a : α), ∃ (x : a ∈ s), p a) ↔ ∃ (a : α), a ∈ s ∧ p a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
s : Finset α
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise.{u_1} (α := ↥s) (r on fun (x : ↥s) ↦ f (↑x : α)) ↔ (↑s : Set α).Pairwise (r on f)

Tactic:
pairwise_subtype_iff_pairwise_set (s : Set α) (r on f)

Premises used: Function.onFun, SetLike.coe, pairwise_subtype_iff_pairwise_set
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
⊢ _root_.Pairwise (α := ↥s) (r on fun (x : ↥s) ↦ (↑x : α)) ↔ (↑s : Set α).Pairwise r

Tactic:
pairwise_subtype_iff_pairwise_finset' r id

Premises used: id, Finset.pairwise_subtype_iff_pairwise_finset'
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ s.max' hs < t.min' ht

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
h : ∀ (x : α), (∀ x_1 ∈ s, x_1 < x) ↔ s.max' hs < x
h₁ : ∀ (x : α), (∀ y ∈ t, x < y) ↔ x < t.min' ht
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all)

Premises used: exists_between
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x : α
⊢ (∀ x_1 ∈ s, x_1 < x) ↔ s.max' hs < x

Tactic:
simp
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x : α
⊢ (∀ y ∈ t, x < y) ↔ x < t.min' ht

Tactic:
simp
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
pos : ∀ (hs : s.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
neg : ∀ (hs : ¬s.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases hs : s.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
neg : ∀ (ht : ¬t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases ht : t.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
neg : ∀ (ht : ¬t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases ht : t.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : t.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
s.exists_between hs ht H

Premises used: Finset.exists_between
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : t.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact s.exists_between hs ht H

Premises used: Finset.exists_between
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
p : α
hp : s.max' hs < p
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact let ⟨p, hp⟩ := exists_gt (s.max' hs); ⟨p, by simp_all⟩
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
p : α
hp : p < t.min' ht
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact let ⟨p, hp⟩ := exists_lt (t.min' ht); ⟨p, by simp_all⟩
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
p : α
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact Nonempty.elim ‹_› fun p ↦ ⟨p, by simp_all⟩

Premises used: Nonempty.elim
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ hsf.toFinset (s := s).Nonempty

Tactic:
simpa
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ htf.toFinset (s := t).Nonempty

Tactic:
simpa
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∀ x ∈ hsf.toFinset (s := s), ∀ y ∈ htf.toFinset (s := t), x < y

Tactic:
simpa
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
h :
  Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
    (∀ x ∈ hsf.toFinset (s := s), x < b) ∧ ∀ y ∈ htf.toFinset (s := t), b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
convert!
    Finset.exists_between (s := hsf.toFinset) (t := htf.toFinset) (by simpa) (by simpa)
      (by simpa) using
    1

Premises used: Finset.exists_between
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
    (∀ x ∈ hsf.toFinset (s := s), x < b) ∧ ∀ y ∈ htf.toFinset (s := t), b < y

Tactic:
simp
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∀ x ∈ hs.toFinset (s := s), ∀ y ∈ ht.toFinset (s := t), x < y

Tactic:
simpa
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
h :
  Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
    (∀ x ∈ hs.toFinset (s := s), x < b) ∧ ∀ y ∈ ht.toFinset (s := t), b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
convert! hs.toFinset.exists_between' ht.toFinset (by simpa) using 1

Premises used: Set.Finite.toFinset, Finset.exists_between'
-- Module: Mathlib.Data.Finset.DenselyOrdered
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
    (∀ x ∈ hs.toFinset (s := s), x < b) ∧ ∀ y ∈ ht.toFinset (s := t), b < y

Tactic:
simp
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ s.dens = HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)

Tactic:
rfl

Premises used: Finset.dens, rfl
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
⊢ dens.{u_2} (α := α) ∅ = 0

Tactic:
simp [dens]

Premises used: Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
a : α
⊢ dens (α := α) {a} = (↑(Fintype.card α) : ℚ≥0)⁻¹

Tactic:
simp [dens]

Premises used: Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).dens = s.dens + (↑(Fintype.card α) : ℚ≥0)⁻¹

Tactic:
simp [dens, add_div]

Premises used: Finset.dens, add_div
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : Disjoint s t
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s.disjUnion t h)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
simp_rw₁ :
  HDiv.hDiv (α := ℚ≥0) (↑(#s + #t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
simp_rw₂ :
  HAdd.hAdd (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (s.disjUnion t h).dens = s.dens + t.dens

Tactic:
simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]

Premises used: Finset.dens, Nat.cast_add, Finset.card_disjUnion, add_div
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ s.dens = 0 ↔ s = ∅

Tactic:
simp +contextual [dens, Fintype.card_eq_zero_iff, eq_empty_of_isEmpty]

Premises used: Finset.dens, Fintype.card_eq_zero_iff, Finset.eq_empty_of_isEmpty
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ s.dens ≠ 0 ↔ s.Nonempty

Tactic:
dens_eq_zero.not.trans nonempty_iff_ne_empty.symm

Premises used: Iff.not, Finset.nonempty_iff_ne_empty, Iff.trans, Finset.dens_eq_zero, Iff.symm
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ 0 < s.dens ↔ s.Nonempty

Tactic:
pos_iff_ne_zero.trans dens_ne_zero

Premises used: Finset.dens_ne_zero, Iff.trans, pos_iff_ne_zero
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : s ⊆ t
⊢ LE.le (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : s ⊂ t
⊢ LT.lt (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : s ⊂ t
⊢ #s < #t

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
⊢ Monotone.{u_2, 0} (α := Finset α) dens

Tactic:
fun _ _ ↦ dens_le_dens

Premises used: Monotone, Finset.dens_le_dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
⊢ StrictMono.{u_2, 0} (α := Finset α) dens

Tactic:
fun _ _ ↦ dens_lt_dens

Premises used: StrictMono, Finset.dens_lt_dens, Set.Subset
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
inl : IsEmpty α → (map f s).dens ≤ s.dens
inr : Nonempty α → (map f s).dens ≤ s.dens
⊢ (map f s).dens ≤ s.dens

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : IsEmpty α
⊢ (map f s).dens ≤ s.dens

Tactic:
simp [Subsingleton.elim s ∅]

Premises used: EmptyCollection.emptyCollection, Subsingleton.elim
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
inr :
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (map f s).dens ≤ s.dens

Tactic:
simp_rw [dens, card_map]

Premises used: Finset.card_map, Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
inr : LT.lt (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)
inr₁ : Fintype.card α ≤ Fintype.card β
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ LT.lt (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)

Tactic:
mod_cast Fintype.card_pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Fintype.card, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Fintype.card_pos, Eq.trans
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ LT.lt (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)

Tactic:
exact mod_cast Fintype.card_pos

Premises used: Fintype.card_pos
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
Fintype.card_le_of_injective _ f.2

Premises used: Fintype.card_le_of_injective, Function.Embedding.inj'
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact Fintype.card_le_of_injective _ f.2

Premises used: Fintype.card_le_of_injective, Function.Embedding.inj'
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
e : α ≃ β
⊢ (map e.toEmbedding s).dens = s.dens

Tactic:
simp [dens, Fintype.card_congr e]

Premises used: Fintype.card_congr, Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
inst_2 : DecidableEq β
f : α → β
hf : Bijective f
s : Finset α
⊢ (image f s).dens = s.dens

Tactic:
simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf)

Premises used: Finset.dens_map_equiv, Finset.map_eq_image, Equiv.ofBijective