awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : ∀ (a : Finset α), a ∈ Iic s ↔ a ∈ s.powerset
⊢ Iic s = s.powerset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s a : Finset α
⊢ a ∈ Iic s ↔ a ∈ s.powerset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : ∀ (a : Finset α), a ∈ Iio s ↔ a ∈ s.ssubsets
⊢ Iio s = s.ssubsets

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s a : Finset α
⊢ a ∈ Iio s ↔ a ∈ s.ssubsets

Tactic:
simp
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
h₁ :
  ∀ (a : Finset α),
    a ∈ @LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t ↔
      Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).powerset) a
⊢ @LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t = image (fun (x : Finset α) ↦ s ∪ x) (t \ s).powerset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
a : Finset α
⊢ a ∈ @LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t ↔
    Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).powerset) a

Tactic:
simp [h, union_comm]

Premises used: Finset.union_comm
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
h₁ :
  ∀ (u : Finset α),
    u ∈ Ico s t ↔ Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets) u
⊢ Ico s t = image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets

Tactic:
ext u
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
h₁ : s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u
⊢ u ∈ Ico s t ↔ Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets) u

Tactic:
simp_rw [mem_Ico, mem_image, mem_ssubsets]

Premises used: Finset.mem_image, Finset.mem_ssubsets, Finset.mem_Ico
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
h₁ : s ≤ u ∧ u < t → ∃ a ⊂ t \ s, s ∪ a = u
h₂ : (∃ a ⊂ t \ s, s ∪ a = u) → s ≤ u ∧ u < t
⊢ s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩

Premises used: sup_sdiff_cancel_right, SDiff.sdiff, And.intro, Exists.intro, sdiff_lt_sdiff_right
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t

Tactic:
⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩

Premises used: le_sup_left, sup_lt_of_lt_sdiff_left, And.intro
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t

Tactic:
exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(@LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t) = HPow.hPow (α := ℕ) 2 (#t - #s)

Tactic:
simp [h, card_sdiff_of_subset]

Premises used: Finset.card_sdiff_of_subset
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 (#t - #s) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
⊢ #(Ico s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]

Premises used: Finset.card_Icc_finset, Finset.card_Ico_eq_card_Icc_sub_one
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 (#t - #s) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
⊢ #(Ioc s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]

Premises used: Finset.card_Icc_finset, Finset.card_Ioc_eq_card_Icc_sub_one
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 2 = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 (#t - #s) - 2 = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
⊢ #(Ioo s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]

Premises used: Finset.card_Icc_finset, Finset.card_Ioo_eq_card_Icc_sub_two
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #s.powerset = HPow.hPow (α := ℕ) 2 #s
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 #s = HPow.hPow (α := ℕ) 2 #s
⊢ #(Iic s) = HPow.hPow (α := ℕ) 2 #s

Tactic:
rw [Iic_eq_powerset, card_powerset]

Premises used: Finset.Iic_eq_powerset, Finset.card_powerset
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #s.ssubsets = HPow.hPow (α := ℕ) 2 #s - 1
rw₁ : #(s.powerset.erase s) = HPow.hPow (α := ℕ) 2 #s - 1
rw₂ : #s.powerset - 1 = HPow.hPow (α := ℕ) 2 #s - 1
rw₃ rw₄ : HPow.hPow (α := ℕ) 2 #s - 1 = HPow.hPow (α := ℕ) 2 #s - 1
⊢ #(Iio s) = HPow.hPow (α := ℕ) 2 #s - 1

Tactic:
rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]

Premises used: Finset.card_erase_of_mem, Finset.ssubsets, Finset.Iio_eq_ssubsets, Finset.mem_powerset_self, Finset.card_powerset
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)

Tactic:
simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]

Premises used: Finset.covBy_iff_exists_cons, monotone_iff_forall_covBy
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)

Tactic:
classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]

Premises used: Finset.covBy_iff_exists_cons, monotone_iff_forall_covBy
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (cons a s ha) ≤ f s

Tactic:
monotone_iff_forall_le_cons (β := βᵒᵈ)

Premises used: Finset.monotone_iff_forall_le_cons, Antitone
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)

Tactic:
simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

Premises used: Finset.covBy_iff_exists_cons, strictMono_iff_forall_covBy
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)

Tactic:
classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

Premises used: Finset.covBy_iff_exists_cons, strictMono_iff_forall_covBy
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
⊢ StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (cons a s ha) < f s

Tactic:
strictMono_iff_forall_lt_cons (β := βᵒᵈ)

Premises used: StrictAnti, Finset.strictMono_iff_forall_lt_cons
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
inst_1 : DecidableEq α
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)

Tactic:
simp [monotone_iff_forall_le_cons]

Premises used: Finset.monotone_iff_forall_le_cons
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
inst_1 : DecidableEq α
⊢ Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) ≤ f s

Tactic:
monotone_iff_forall_le_insert (β := βᵒᵈ)

Premises used: Finset.monotone_iff_forall_le_insert, Antitone
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
inst_1 : DecidableEq α
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)

Tactic:
simp [strictMono_iff_forall_lt_cons]

Premises used: Finset.strictMono_iff_forall_lt_cons
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f : Finset α → β
inst_1 : DecidableEq α
⊢ StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) < f s

Tactic:
strictMono_iff_forall_lt_insert (β := βᵒᵈ)

Premises used: Finset.strictMono_iff_forall_lt_insert, StrictAnti
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α → Finset α) max Union.union

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ⊔ t = s ∪ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α → Finset α) min Inter.inter

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ⊓ t = s ∩ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t).val = s.val.ndunion t.val

Tactic:
rfl

Premises used: Multiset.ndunion, rfl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t).val = s.val ∪ t.val

Tactic:
ndunion_eq_union s.2

Premises used: Multiset.ndunion_eq_union, Finset.nodup, Multiset.ndunion
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

Tactic:
mem_ndunion

Premises used: Set.Mem, setOf, Multiset.mem_ndunion, Multiset.Mem, Multiset.ndunion
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ s
⊢ a ∈ s ∪ t

Tactic:
mem_union.2 <| Or.inl h

Premises used: Iff.mpr, Finset.mem_union, Or.inl
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
t : Finset α
a : α
s : Finset α
h : a ∈ t
⊢ a ∈ s ∪ t

Tactic:
mem_union.2 <| Or.inr h

Premises used: Iff.mpr, Finset.mem_union, Or.inr
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
p : α → Prop
⊢ (∀ (a : α), a ∈ s ∪ t → p a) ↔ (∀ (a : α), a ∈ s → p a) ∧ ∀ (a : α), a ∈ t → p a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
rw : ¬(a ∈ s ∨ a ∈ t) ↔ ¬a ∈ s ∧ ¬a ∈ t
rw₁ rw₂ : ¬a ∈ s ∧ ¬a ∈ t ↔ ¬a ∈ s ∧ ¬a ∈ t
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t

Tactic:
rw [mem_union, not_or]

Premises used: not_or, Finset.mem_union
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (↑(s₁ ∪ s₂) : Set α) = (↑s₁ : Set α) ∪ (↑s₂ : Set α)

Tactic:
Set.ext fun _ => mem_union

Premises used: Set.ext, Finset.mem_union
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
hs : s ⊆ u
⊢ t ⊆ u → s ∪ t ⊆ u

Tactic:
sup_le <| le_iff_subset.2 hs

Premises used: Iff.mpr, Set.Mem, setOf, sup_le, Finset.le_iff_subset
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ⊆ s₁ ∪ s₂

Tactic:
fun _ ↦ mem_union_left _

Premises used: Finset.mem_union_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₂ ⊆ s₁ ∪ s₂

Tactic:
fun _ ↦ mem_union_right _

Premises used: Finset.mem_union_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u v : Finset α
hsu : s ⊆ u
htv : t ⊆ v
⊢ s ∪ t ⊆ u ∪ v

Tactic:
sup_le_sup (le_iff_subset.2 hsu) htv

Premises used: Iff.mpr, sup_le_sup, Set.Mem, setOf, Finset.le_iff_subset
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ t : Finset α
h : s₁ ⊆ s₂
⊢ s₁ ∪ t ⊆ s₂ ∪ t

Tactic:
union_subset_union h Subset.rfl

Premises used: Finset.Subset.rfl, Finset.union_subset_union
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t₁ t₂ : Finset α
h : t₁ ⊆ t₂
⊢ s ∪ t₁ ⊆ s ∪ t₂

Tactic:
union_subset_union Subset.rfl h

Premises used: Finset.Subset.rfl, Finset.union_subset_union
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∪ s₂ = s₂ ∪ s₁

Tactic:
sup_comm _ _

Premises used: sup_comm
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a : α
⊢ Std.Commutative fun (x1 x2 : Finset α) ↦ x1 ∪ x2

Tactic:
⟨union_comm⟩

Premises used: Finset.union_comm, Std.Commutative.mk
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

Tactic:
sup_assoc _ _ _

Premises used: sup_assoc
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a : α
⊢ Std.Associative fun (x1 x2 : Finset α) ↦ x1 ∪ x2

Tactic:
⟨union_assoc⟩

Premises used: Finset.union_assoc, Std.Associative.mk
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s ∪ s = s

Tactic:
sup_idem _

Premises used: sup_idem
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a : α
⊢ Std.IdempotentOp fun (x1 x2 : Finset α) ↦ x1 ∪ x2

Tactic:
⟨union_idempotent⟩

Premises used: Finset.union_idempotent, Std.IdempotentOp.mk
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : s ∪ t ⊆ u
⊢ s ⊆ u

Tactic:
subset_union_left.trans h

Premises used: HasSubset.Subset.trans, Finset.subset_union_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : s ∪ t ⊆ u
⊢ t ⊆ u

Tactic:
Subset.trans subset_union_right h

Premises used: Finset.Subset.trans, Finset.subset_union_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ (t ∪ u) ↔ x ∈ t ∪ (s ∪ u)

Tactic:
simp only [mem_union, or_left_comm]

Premises used: or_left_comm, Finset.mem_union
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t

Tactic:
simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

Premises used: Finset.mem_union, or_comm, or_assoc
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s ∪ s = s

Tactic:
union_idempotent s

Premises used: Finset.union_idempotent
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t = s ↔ t ⊆ s

Tactic:
sup_eq_left

Premises used: sup_eq_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : s ∪ t = s ↔ t ⊆ s
rw₁ rw₂ : t ⊆ s ↔ t ⊆ s
⊢ s = s ∪ t ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_left]

Premises used: Finset.union_eq_left, eq_comm
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t = t ↔ s ⊆ t

Tactic:
sup_eq_right

Premises used: sup_eq_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∪ s = s ↔ t ⊆ s
rw₁ rw₂ : t ⊆ s ↔ t ⊆ s
⊢ s = t ∪ s ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_right]

Premises used: eq_comm, Finset.union_eq_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
ht : t ⊆ s ∪ u
hu : u ⊆ s ∪ t
⊢ s ∪ t = s ∪ u

Tactic:
sup_congr_left ht hu

Premises used: sup_congr_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
hs : s ⊆ t ∪ u
ht : t ⊆ s ∪ u
⊢ s ∪ u = t ∪ u

Tactic:
sup_congr_right hs ht

Premises used: sup_congr_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

Tactic:
sup_eq_sup_iff_left

Premises used: sup_eq_sup_iff_left, Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

Tactic:
sup_eq_sup_iff_right

Premises used: Set.Mem, setOf, sup_eq_sup_iff_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (s₁ ∩ s₂).val = s₁.val.ndinter s₂.val

Tactic:
rfl

Premises used: Multiset.ndinter, rfl, Multiset.filter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (s₁ ∩ s₂).val = s₁.val ∩ s₂.val

Tactic:
ndinter_eq_inter s₁.2

Premises used: Finset.nodup, Multiset.ndinter_eq_inter, Multiset.ndinter, Multiset.filter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s₁ s₂ : Finset α
⊢ a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂

Tactic:
mem_ndinter

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.ndinter, Multiset.mem_ndinter, Multiset.filter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s₁ s₂ : Finset α
h : a ∈ s₁ ∩ s₂
⊢ a ∈ s₁

Tactic:
(mem_inter.1 h).1

Premises used: And.left, Iff.mp, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s₁ s₂ : Finset α
h : a ∈ s₁ ∩ s₂
⊢ a ∈ s₂

Tactic:
(mem_inter.1 h).2

Premises used: And.right, Iff.mp, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s₁ s₂ : Finset α
⊢ a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂

Tactic:
and_imp.1 mem_inter.2

Premises used: Iff.mpr, and_imp, Iff.mp, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ s₂ ⊆ s₁

Tactic:
fun _ ↦ mem_of_mem_inter_left

Premises used: Finset.mem_of_mem_inter_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ s₂ ⊆ s₂

Tactic:
fun _ ↦ mem_of_mem_inter_right

Premises used: Finset.mem_of_mem_inter_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (↑(s₁ ∩ s₂) : Set α) = (↑s₁ : Set α) ∩ (↑s₂ : Set α)

Tactic:
Set.ext fun _ => mem_inter

Premises used: Set.ext, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ s = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ t = t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ s₂ = s₂ ∩ s₁

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s ∩ s = s

Tactic:
ext fun _ => mem_inter.trans <| and_self_iff

Premises used: Finset.ext, Iff.trans, and_self_iff, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : (t ∪ s) ∩ s = s
rw₁ rw₂ : s = s
⊢ s ∩ (t ∪ s) = s

Tactic:
rw [inter_comm, union_inter_cancel_right]

Premises used: Finset.inter_comm, Finset.union_inter_cancel_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
⊢ x ∩ s ⊆ y ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : t ⊆ u
⊢ s ∩ t ⊆ s ∩ u

Tactic:
inter_subset_inter Subset.rfl h

Premises used: Finset.Subset.rfl, Finset.inter_subset_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ s ∩ u ⊆ t ∩ u

Tactic:
inter_subset_inter h Subset.rfl

Premises used: Finset.Subset.rfl, Finset.inter_subset_inter
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∩ t ⊆ s ∪ t

Tactic:
le_iff_subset.1 inf_le_sup

Premises used: inf_le_sup, Iff.mp, Finset.le_iff_subset
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a_1 : α
a b c : Finset α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
simp +contextual only
        [sup_eq_union, inf_eq_inter, le_eq_subset, subset_iff, mem_inter, mem_union, and_imp,
        or_imp, true_or, imp_true_iff, true_and, or_true]

Premises used: true_or, and_imp, Finset.inf_eq_inter, or_imp, imp_true_iff, Finset.subset_iff, Finset.le_eq_subset, Finset.mem_union, Finset.mem_inter, Finset.sup_eq_union, or_true, true_and
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ (s ∪ t) = s ∪ t

Tactic:
sup_left_idem _ _

Premises used: sup_left_idem
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t ∪ t = s ∪ t

Tactic:
sup_right_idem _ _

Premises used: sup_right_idem
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∩ (s ∩ t) = s ∩ t

Tactic:
inf_left_idem _ _

Premises used: inf_left_idem
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∩ t ∩ t = s ∩ t

Tactic:
inf_right_idem _ _

Premises used: inf_right_idem
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Tactic:
inf_sup_left _ _ _

Premises used: inf_sup_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Tactic:
inf_sup_right _ _ _

Premises used: inf_sup_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Tactic:
sup_inf_left _ _ _

Premises used: sup_inf_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Tactic:
sup_inf_right _ _ _

Premises used: sup_inf_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

Tactic:
sup_sup_distrib_left _ _ _

Premises used: sup_sup_distrib_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

Tactic:
sup_sup_distrib_right _ _ _

Premises used: sup_sup_distrib_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

Tactic:
inf_inf_distrib_left _ _ _

Premises used: inf_inf_distrib_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

Tactic:
inf_inf_distrib_right _ _ _

Premises used: inf_inf_distrib_right