awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₂ : insert a (↑s : Set α) ⊆ insert a (↑t : Set α) ↔ s ⊆ t
rwa₃ : (↑s : Set α) ⊆ (↑t : Set α) ↔ s ⊆ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa₄ : a ∉ (↑s : Set α)
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₂ : insert a (↑s : Set α) ⊆ insert a (↑t : Set α) ↔ s ⊆ t
rwa₃ : (↑s : Set α) ⊆ (↑t : Set α) ↔ s ⊆ t
rwa₄ : a ∉ (↑s : Set α)
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa₅ : s ⊆ t ↔ s ⊆ t
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
⊢ consPiProd f has (prodPiCons f has x) = x
have fst : (consPiProd f has (prodPiCons f has x)).1 = x.1
Tactic: ext _ hi
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
fst : (consPiProd f has (prodPiCons f has x)).1 = x.1
⊢ consPiProd f has (prodPiCons f has x) = x
have snd : ∀ (x_1 : α) (hi : x_1 ∈ s), (consPiProd f has (prodPiCons f has x)).2 x_1 hi = x.2 x_1 hi
Tactic: ext _ hi
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup
have rw : (insert a s).val = ndinsert a s.val
Tactic: rw [dedup_cons, dedup_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).val = a ::ₘ s.val
have rw : ndinsert a s.val = a ::ₘ s.val
Tactic: rw [insert_val, ndinsert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
rw : ndinsert a s.val = a ::ₘ s.val
⊢ (insert a s).val = a ::ₘ s.val
have rw₁ : a ::ₘ s.val = a ::ₘ s.val
Tactic: rw [insert_val, ndinsert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ (↑s : Set α) = {a, b} ↔ s = {a, b}
have rw : (↑s : Set α) = (↑{a, b} : Set α) ↔ s = {a, b}
Tactic: rw [← coe_pair, coe_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
rw : (↑s : Set α) = (↑{a, b} : Set α) ↔ s = {a, b}
⊢ (↑s : Set α) = {a, b} ↔ s = {a, b}
have rw₁ : s = {a, b} ↔ s = {a, b}
Tactic: rw [← coe_pair, coe_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ≠ insert a t
have contrapose : ∀ (h : s = insert a t), a ∈ s
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive { val := a ::ₘ s, nodup := nd }
have cons₁ : motive (Finset.cons a { val := s, nodup := sorry } sorry)
Tactic: rw [mk_cons nd]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
⊢ motive { val := s, nodup := nd }
have empty₁ : ∀ (nd : Nodup.{u_3} (α := α) 0), motive { val := 0, nodup := nd }
Tactic: induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)
Cleared hypotheses: s, nd
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
empty₁ : ∀ (nd : Nodup.{u_3} (α := α) 0), motive { val := 0, nodup := nd }
⊢ motive { val := s, nodup := nd }
have cons₁ : ∀ (a : α) (s : Multiset α) (IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }) (nd : (a ::ₘ s).Nodup),
  motive { val := a ::ₘ s, nodup := nd }
Tactic: induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)
Cleared hypotheses: s, nd
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
⊢ motive (Finset.cons a t ha) hs
have cons₁ : ∀ (ha : a ∉ ∅) (h : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs) (hs : (Finset.cons a ∅ ha).Nonempty),
  motive (Finset.cons a ∅ ha) hs
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
Cleared hypotheses: t, ha, h, hs
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
cons₁ :
  ∀ (ha : a ∉ ∅) (h : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs) (hs : (Finset.cons a ∅ ha).Nonempty),
    motive (Finset.cons a ∅ ha) hs
⊢ motive (Finset.cons a t ha) hs
have cons₂ : ∀ (ht : t.Nonempty), motive (Finset.cons a t ha) hs
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
⊢ motive s hs
have empty : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs
Tactic: induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
empty : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs
⊢ motive s hs
have cons₁ : ∀ (a : α) (t : Finset α) (ha : a ∉ t) (h : ∀ (hs : t.Nonempty), motive t hs) (hs : (Finset.cons a t ha).Nonempty),
  motive (Finset.cons a t ha) hs
Tactic: induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
⊢ insertPiProd f (prodPiInsert f x) = x
have fst : (insertPiProd f (prodPiInsert f x)).1 = x.1
Tactic: ext _ hi
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
fst : (insertPiProd f (prodPiInsert f x)).1 = x.1
⊢ insertPiProd f (prodPiInsert f x) = x
have snd : ∀ (x_1 : α) (hi : x_1 ∈ s), (insertPiProd f (prodPiInsert f x)).2 x_1 hi = x.2 x_1 hi
Tactic: ext _ hi
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Finset α) (toFinset {a}) {a}
have rw : (a ::ₘ 0).toFinset = {a}
Tactic: rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw : (a ::ₘ 0).toFinset = {a}
⊢ Eq (α := Finset α) (toFinset {a}) {a}
have rw₁ : Eq (α := Finset α) (insert a (toFinset 0)) {a}
Tactic: rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw : (a ::ₘ 0).toFinset = {a}
rw₁ : Eq (α := Finset α) (insert a (toFinset 0)) {a}
⊢ Eq (α := Finset α) (toFinset {a}) {a}
have rw₂ : Eq (α := Finset α) (insert a ∅) {a}
Tactic: rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw : (a ::ₘ 0).toFinset = {a}
rw₁ : Eq (α := Finset α) (insert a (toFinset 0)) {a}
rw₂ : Eq (α := Finset α) (insert a ∅) {a}
⊢ Eq (α := Finset α) (toFinset {a}) {a}
have rw₃ : Eq (α := Finset α) {a} {a}
Tactic: rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val
have pos : ∀ (h : a ∈ l), (a :: l).toFinset.val = (insert a l.toFinset).val
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
pos : ∀ (h : a ∈ l), (a :: l).toFinset.val = (insert a l.toFinset).val
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val
have neg : ∀ (h : a ∉ l), (a :: l).toFinset.val = (insert a l.toFinset).val
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}
have h : ∀ (x : α), x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) {a} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.toFinset = ∅ ↔ l = []
have nil : Eq.{u_1 + 1} (α := Finset α) (toFinset []) ∅ ↔ Eq.{u_1 + 1} (α := List α) [] []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := Finset α) (toFinset []) ∅ ↔ Eq.{u_1 + 1} (α := List α) [] []
⊢ l.toFinset = ∅ ↔ l = []
have cons : ∀ (head : α) (tail : List α), (head :: tail).toFinset = ∅ ↔ head :: tail = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
a : α
s : Finset α
⊢ s.toList = [a] ↔ s = {a}
have rw : s.val.toList = [a] ↔ s = {a}
Tactic: rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
a : α
s : Finset α
rw : s.val.toList = [a] ↔ s = {a}
⊢ s.toList = [a] ↔ s = {a}
have rw₁ : s.val = {a} ↔ s = {a}
Tactic: rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
a : α
s : Finset α
rw : s.val.toList = [a] ↔ s = {a}
rw₁ : s.val = {a} ↔ s = {a}
⊢ s.toList = [a] ↔ s = {a}
have rw₂ : s = {a} ↔ s = {a}
Tactic: rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise.{u_1} (α := ↥(cons a s ha)) (r on fun (a_1 : ↥(cons a s ha)) ↦ f (↑a_1 : α)) ↔
    _root_.Pairwise.{u_1} (α := ↥s) (r on fun (a : ↥s) ↦ f (↑a : α)) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
have simp : ((↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ (↑s : Set α), a ≠ b → (r on f) a b ∧ (r on f) b a) ↔
  (↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
Tactic: simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
have pos : ∀ (hst : s ⊆ t),
  Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s sorry, inj' := sorry }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
Tactic: by_cases hst : s ⊆ t
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
pos :
  ∀ (hst : s ⊆ t),
    Membership.mem (γ := Finset (Finset α))
        ((fun (s t : Finset α) ↦
            (if s ⊆ t then
                map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                  (t \ s).powerset.attach
              else ∅ :
              Finset (Finset α)))
          s t)
        u ↔
      s ≤ u ∧ u ≤ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
have neg : ∀ (hst : ¬s ⊆ t),
  Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s sorry, inj' := sorry }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
Tactic: by_cases hst : s ⊆ t
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
have pos : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
Tactic: suffices (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t by
          simpa [hst, subset_sdiff, and_assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
have pos : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) → s ⊆ u ∧ u ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
pos : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) → s ⊆ u ∧ u ⊆ t
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
have pos₁ : s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t
have neg : s ⊆ u → ¬u ⊆ t
Tactic: suffices s ⊆ u → ¬u ⊆ t by simpa [hst]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Icc s t = {u ∈ t.powerset | s ⊆ u}
have h : ∀ (a : Finset α), a ∈ Icc s t ↔ a ∈ {u ∈ t.powerset | s ⊆ u}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Ico s t = {u ∈ t.ssubsets | s ⊆ u}
have h : ∀ (a : Finset α), a ∈ Ico s t ↔ a ∈ {u ∈ t.ssubsets | s ⊆ u}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Ioc s t = {u ∈ t.powerset | s ⊂ u}
have h : ∀ (a : Finset α), a ∈ Ioc s t ↔ a ∈ {u ∈ t.powerset | s ⊂ u}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Ioo s t = {u ∈ t.ssubsets | s ⊂ u}
have h : ∀ (a : Finset α), a ∈ Ioo s t ↔ a ∈ {u ∈ t.ssubsets | s ⊂ u}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ Iic s = s.powerset
have h : ∀ (a : Finset α), a ∈ Iic s ↔ a ∈ s.powerset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ Iio s = s.ssubsets
have h : ∀ (a : Finset α), a ∈ Iio s ↔ a ∈ s.ssubsets
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ @LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t = image (fun (x : Finset α) ↦ s ∪ x) (t \ s).powerset
have h₁ : ∀ (a : Finset α),
  a ∈ @LocallyFiniteOrder.finsetIcc _ PartialOrder.toPreorder _ s t ↔
    Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).powerset) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Ico s t = image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets
have h₁ : ∀ (u : Finset α),
  u ∈ Ico s t ↔ Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets) u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Ico s t ↔ Membership.mem (γ := Finset (Finset α)) (image (fun (x : Finset α) ↦ s ∪ x) (t \ s).ssubsets) u
have h₁ : s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u
Tactic: simp_rw [mem_Ico, mem_image, mem_ssubsets]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u
have h₁ : s ≤ u ∧ u < t → ∃ a ⊂ t \ s, s ∪ a = u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
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
⊢ s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u
have h₂ : (∃ a ⊂ t \ s, s ∪ a = u) → s ≤ u ∧ u < t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ico s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
have rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
⊢ #(Ico s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
have rw₁ : HPow.hPow (α := ℕ) 2 (#t - #s) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ioc s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
have rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
⊢ #(Ioc s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
have rw₁ : HPow.hPow (α := ℕ) 2 (#t - #s) - 1 = HPow.hPow (α := ℕ) 2 (#t - #s) - 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ioo s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
have rw : #(Icc s t) - 2 = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
rw : #(Icc s t) - 2 = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
⊢ #(Ioo s t) = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
have rw₁ : HPow.hPow (α := ℕ) 2 (#t - #s) - 2 = HPow.hPow (α := ℕ) 2 (#t - #s) - 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ #(Iic s) = HPow.hPow (α := ℕ) 2 #s
have rw : #s.powerset = HPow.hPow (α := ℕ) 2 #s
Tactic: rw [Iic_eq_powerset, card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #s.powerset = HPow.hPow (α := ℕ) 2 #s
⊢ #(Iic s) = HPow.hPow (α := ℕ) 2 #s
have rw₁ : HPow.hPow (α := ℕ) 2 #s = HPow.hPow (α := ℕ) 2 #s
Tactic: rw [Iic_eq_powerset, card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ #(Iio s) = HPow.hPow (α := ℕ) 2 #s - 1
have rw : #s.ssubsets = HPow.hPow (α := ℕ) 2 #s - 1
Tactic: rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #s.ssubsets = HPow.hPow (α := ℕ) 2 #s - 1
⊢ #(Iio s) = HPow.hPow (α := ℕ) 2 #s - 1
have rw₁ : #(s.powerset.erase s) = HPow.hPow (α := ℕ) 2 #s - 1
Tactic: rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
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
⊢ #(Iio s) = HPow.hPow (α := ℕ) 2 #s - 1
have rw₂ : #s.powerset - 1 = HPow.hPow (α := ℕ) 2 #s - 1
Tactic: rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Interval (goal)
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
⊢ #(Iio s) = HPow.hPow (α := ℕ) 2 #s - 1
have rw₃ : HPow.hPow (α := ℕ) 2 #s - 1 = HPow.hPow (α := ℕ) 2 #s - 1
Tactic: rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t
have rw : ¬(a ∈ s ∨ a ∈ t) ↔ ¬a ∈ s ∧ ¬a ∈ t
Tactic: rw [mem_union, not_or]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
rw : ¬(a ∈ s ∨ a ∈ t) ↔ ¬a ∈ s ∧ ¬a ∈ t
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t
have rw₁ : ¬a ∈ s ∧ ¬a ∈ t ↔ ¬a ∈ s ∧ ¬a ∈ t
Tactic: rw [mem_union, not_or]