awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
rw rw₁ :
  (H s fun (t : Finset α) (h : t ⊂ s) ↦
      have this := ⋯;
      strongInduction (p := fun (x : Finset α) ↦ p x) H t) =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t
⊢ strongInduction (p := fun (x : Finset α) ↦ p x) H s =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t

Tactic:
rw [strongInduction]

Premises used: Finset.strongInduction
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset α → Prop
s : Finset α
h₀ : p ∅
h₁ : ∀ (a : α) (s : Finset α), a ∉ s → (∀ t ⊆ s, p t) → p (insert a s)
⊢ p s

Tactic:
Finset.strongInductionOn s fun s =>
    Finset.induction_on s (fun _ => h₀) fun a s n _ ih =>
      (h₁ a s n) fun t ss => ih _ (lt_of_le_of_lt ss (ssubset_insert n) : t < _)

Premises used: Finset.strongInductionOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs : s.Nonempty
inl : ∀ (a : α) (hs : Finset.Nonempty (α := α) {a}), p {a} hs
inr : ∀ (hs_1 : s.Nontrivial), p s hs
⊢ p s hs

Tactic:
obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial

Premises used: Finset.Nonempty.exists_eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
a : α
hs : Finset.Nonempty (α := α) {a}
⊢ p {a} hs

Tactic:
h₀ _
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
a : α
hs : Finset.Nonempty (α := α) {a}
⊢ p {a} hs

Tactic:
exact h₀ _
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
⊢ p s hs_1

Tactic:
h₁ hs fun t ht hts ↦ ?_
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
inr : ∀ (t : Finset α) (ht : t.Nonempty) (hts : t ⊂ s), p t ht
⊢ p s hs_1

Tactic:
refine h₁ hs fun t ht hts ↦ ?_
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
inr : ∀ (this : #t < #s), p t ht
⊢ p t ht

Tactic:
have := card_lt_card hts
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
this : #t < #s
⊢ p t ht

Tactic:
ht.strong_induction h₀ h₁
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
this : #t < #s
⊢ p t ht

Tactic:
exact ht.strong_induction h₀ h₁
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
s_1 t_1 u : Finset α
f : α → β
n_1 : ℕ
p : Finset α → Sort u_4
n : ℕ
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
x : Finset α
s : Finset α := x
t : Finset α
ht : #t ≤ n
h : s ⊂ t
this : #s < #t
⊢ n - #t < n - #s

Tactic:
lia
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
rw rw₁ :
  (H s fun {t : Finset α} (ht : #t ≤ n) (h : s ⊂ t) ↦
      have this := ⋯;
      have this := ⋯;
      strongDownwardInduction (p := p) H t ht) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := p) H t ht
⊢ strongDownwardInduction (p := p) H s =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := p) H t ht

Tactic:
rw [strongDownwardInduction]

Premises used: Finset.strongDownwardInduction
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
dsimp :
  (fun (a : #s ≤ n) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H s a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht
⊢ (fun (a : #s ≤ n) ↦ s.strongDownwardInductionOn (p := fun (x : Finset α) ↦ p x) H a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ t.strongDownwardInductionOn (p := fun (x : Finset α) ↦ p x) H ht

Tactic:
dsimp only [strongDownwardInductionOn]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
rw rw₁ :
  (fun (a : #s ≤ n) ↦
      H s
        (fun {t : Finset α} (ht : #t ≤ n) (h : s ⊂ t) ↦
          have this := ⋯;
          have this := ⋯;
          strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht)
        a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht
⊢ (fun (a : #s ≤ n) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H s a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht

Tactic:
rw [strongDownwardInduction]

Premises used: Finset.strongDownwardInduction
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_4
⊢ WellFounded.{u_4 + 1} (α := Finset α) LT.lt

Tactic:
have H : Subrelation (@LT.lt (Finset α) _) (InvImage (· < ·) card) := fun {_ _} hxy =>
    card_lt_card hxy
  Subrelation.wf H <| InvImage.wf _ <| (Nat.lt_wfRel).2

Premises used: Subrelation.wf, Finset.card_lt_card, WellFoundedRelation.wf, Finset.card, InvImage.wf
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset α → Prop
H : ∀ (S : Finset α), (∀ s ∈ S, p (S.erase s)) → p S
S : Finset α
⊢ p S

Tactic:
S.strongInduction fun S ih => H S fun _ hs => ih _ (erase_ssubset hs)

Premises used: Finset.erase, Finset.erase_ssubset, Finset.strongInduction
-- Module: Mathlib.Data.Finset.CastCard
Goal:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
hs : a ∈ s
rw : (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#(s.erase a) + 1) : R) 1
rw₁ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) (↑1 : R) - 1
rw₂ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1 - 1
rw₃ rw₄ : HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1 = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1
⊢ (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#s) : R) 1

Tactic:
rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]

Premises used: Finset.card_erase_add_one, eq_sub_iff_add_eq, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Finset.CastCard
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∩ t)) : R) (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∩ t) + #(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₃ rw₄ : HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∪ t)) : R)

Tactic:
rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]

Premises used: eq_sub_iff_add_eq, Nat.cast_add, Finset.card_inter_add_card_union
-- Module: Mathlib.Data.Finset.CastCard
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∪ t)) : R) (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∪ t) + #(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₃ rw₄ : HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∩ t)) : R)

Tactic:
rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]

Premises used: eq_sub_iff_add_eq, Finset.card_union_add_card_inter, Nat.cast_add
-- Module: Mathlib.Data.Finset.CastCard
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
h : s ⊆ t
rw : (↑(#t - #s) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
rw₁ rw₂ : HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
⊢ (↑(#(t \ s)) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)

Tactic:
rw [card_sdiff_of_subset h, Nat.cast_sub (card_mono h)]

Premises used: Nat.cast_sub, Finset.card_sdiff_of_subset, Finset.card_mono
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s.val.dedup = s.val

Tactic:
s.2.dedup

Premises used: Finset.nodup, Multiset.Nodup.dedup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.toFinset.val = s.dedup

Tactic:
rfl

Premises used: Multiset.dedup, rfl
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : s.Nodup
⊢ { val := s, nodup := n : Finset α } = s.toFinset

Tactic:
Finset.val_inj.1 n.dedup.symm

Premises used: Iff.mp, Multiset.Nodup.dedup, Eq.symm, Finset.val_inj
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'

Tactic:
simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

Premises used: Multiset.toFinset_eq
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s.toFinset ↔ a ∈ s

Tactic:
mem_dedup

Premises used: Set.Mem, Multiset.dedup, setOf, Multiset.mem_dedup, Multiset.Mem
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

Premises used: Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp_rw [Finset.ssubset_def, toFinset_subset]

Premises used: Finset.ssubset_def, Multiset.toFinset_subset
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s t : Multiset α
⊢ IsWellFounded.{u_2} (Multiset β) fun (x1 x2 : Multiset β) ↦ x1 ⊂ x2

Tactic:
Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

Premises used: Multiset.toFinset, Iff.mpr, InvImage, Multiset.toFinset_ssubset, Subrelation.isWellFounded
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s t : Multiset α
⊢ IsWellFounded.{u_2} (Multiset β) fun (x1 x2 : Multiset β) ↦ x1 ⊂ x2

Tactic:
exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

Premises used: Multiset.toFinset, Iff.mpr, InvImage, Multiset.toFinset_ssubset, Subrelation.isWellFounded
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s t : Multiset α
⊢ IsWellFounded.{u_2} (Multiset β) fun (x1 x2 : Multiset β) ↦ x1 ⊂ x2

Tactic:
classical
  exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

Premises used: Multiset.toFinset, Iff.mpr, InvImage, Multiset.toFinset_ssubset, Subrelation.isWellFounded
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : ∀ (a : α), a ∈ s.val.toFinset ↔ a ∈ s
⊢ s.val.toFinset = s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∈ s.val ↔ a ∈ s
h₁ h₂ : a ∈ s ↔ a ∈ s
⊢ a ∈ s.val.toFinset ↔ a ∈ s

Tactic:
rw [Multiset.mem_toFinset, ← mem_def]

Premises used: Multiset.mem_toFinset, Finset.mem_def
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
a : Finset α
b : Multiset α
⊢ a.val ≤ b ↔ a.val ⊆ b

Tactic:
Multiset.le_iff_subset a.nodup

Premises used: Multiset.le_iff_subset, Finset.nodup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.toFinset.val = (↑l.dedup : Multiset α)

Tactic:
rfl

Premises used: Multiset.dedup, Multiset.ofList, rfl
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ (↑l : Multiset α).toFinset = l.toFinset

Tactic:
rfl

Premises used: List.toFinset, rfl
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
n rwa rwa₁ rwa₂ rwa₃ : l.Nodup
⊢ (↑l : Multiset α).Nodup

Tactic:
rwa [Multiset.coe_nodup]

Premises used: Multiset.coe_nodup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
⊢ a ∈ l.toFinset ↔ a ∈ l

Tactic:
mem_dedup

Premises used: Set.Mem, setOf, List.mem_dedup, Multiset.Mem
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ (↑l.toFinset : Set α) = {a : α | a ∈ l}

Tactic:
Set.ext fun _ => List.mem_toFinset

Premises used: List.mem_toFinset, Set.ext
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
h :
  Membership.mem (γ := Set (Finset α)) Set.univ
    { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hl : Finset α }
⊢ Membership.mem (γ := Set (Finset α)) (toFinset '' {l : List α | l.Nodup})
    { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hl : Finset α }

Tactic:
⟨l, hl, (toFinset_eq hl).symm⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, List.toFinset_eq, Eq.symm
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
h :
  Membership.mem (γ := Set (Finset α)) Set.univ
    { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hl : Finset α }
⊢ Membership.mem (γ := Set (Finset α)) (toFinset '' {l : List α | l.Nodup})
    { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hl : Finset α }

Tactic:
exact ⟨l, hl, (toFinset_eq hl).symm⟩
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := List α) toFinset

Tactic:
fun s =>
  let ⟨l, _, hls⟩ := toFinset_surj_on (Set.mem_univ s)
  ⟨l, hls⟩

Premises used: Exists, _private.0.List.toFinset_surjective.match_1, List.toFinset, List.toFinset_surj_on, Exists.intro, Set.mem_univ, Eq, Function.Surjective
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup

Tactic:
simp [Finset.ext_iff, perm_ext_iff_of_nodup (nodup_dedup _) (nodup_dedup _)]

Premises used: Finset.ext_iff, List.nodup_dedup, List.perm_ext_iff_of_nodup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
⊢ a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

Tactic:
simp only [Finset.ext_iff, mem_toFinset]

Premises used: List.mem_toFinset, Finset.ext_iff
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ (∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset

Tactic:
toFinset.ext_iff.mpr

Premises used: List.toFinset.ext_iff, Iff.mpr
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~ l'
⊢ l.toFinset = l'.toFinset

Tactic:
toFinset_eq_iff_perm_dedup.mpr h.dedup

Premises used: Iff.mpr, List.Perm.dedup, List.toFinset_eq_iff_perm_dedup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
rw : (↑l : Multiset α) = (↑l' : Multiset α)
⊢ l ~ l'

Tactic:
rw [← Multiset.coe_eq_coe]

Premises used: Multiset.coe_eq_coe
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ (↑l : Multiset α) = (↑l' : Multiset α)

Tactic:
Multiset.Nodup.toFinset_inj hl hl' h

Premises used: Multiset.Nodup.toFinset_inj
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ (↑l : Multiset α) = (↑l' : Multiset α)

Tactic:
exact Multiset.Nodup.toFinset_inj hl hl' h
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.reverse.toFinset = l.toFinset

Tactic:
toFinset_eq_of_perm _ _ (reverse_perm l)

Premises used: List.toFinset_eq_of_perm, List.reverse_perm
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
s : Finset α
rw : s.val.Nodup
⊢ s.toList.Nodup

Tactic:
rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]

Premises used: Multiset.coe_toList, Multiset.coe_nodup, Finset.toList
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
s : Finset α
⊢ s.val.Nodup

Tactic:
s.nodup

Premises used: Finset.nodup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
s : Finset α
⊢ s.val.Nodup

Tactic:
exact s.nodup

Premises used: Finset.nodup
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
a : α
s : Finset α
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
Multiset.mem_toList

Premises used: Set.Mem, setOf, Finset.toList, Multiset.Mem, Multiset.mem_toList
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
s : Finset α
⊢ (↑s.toList : Multiset α) = s.val

Tactic:
s.val.coe_toList

Premises used: Multiset.coe_toList, Finset.toList, Finset.val
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : ∀ (a : α), a ∈ s.toList.toFinset ↔ a ∈ s
⊢ s.toList.toFinset = s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ a ∈ s.toList.toFinset ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
hs : s.Nodup
apply : s.toFinset.toList.toFinset = s.toFinset
⊢ s.toFinset.toList.Perm s

Tactic:
apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs

Premises used: List.perm_of_nodup_nodup_toFinset_eq, Finset.nodup_toList
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
hs : s.Nodup
rw rw₁ : s.toFinset = s.toFinset
⊢ s.toFinset.toList.toFinset = s.toFinset

Tactic:
rw [toList_toFinset]

Premises used: Finset.toList_toFinset
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ ∃ (l : List α), l.Nodup ∧ l.toFinset = s

Tactic:
⟨s.toList, s.nodup_toList, s.toList_toFinset⟩

Premises used: Finset.nodup_toList, Finset.toList_toFinset, Finset.toList, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Dedup
Goal:
α : Type u_1
f₁ f₂ : Finset α
h : f₁.toList.Perm f₂.toList
x : α
⊢ x ∈ f₁ ↔ x ∈ f₂

Tactic:
simp [← Finset.mem_toList, h.mem_iff]

Premises used: Finset.mem_toList, List.Perm.mem_iff
-- Module: Mathlib.Data.Finset.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ CanLift.{u_4 + 1, u_4 + 1} (Multiset α) (Finset α) Finset.val Nodup

Tactic:
⟨fun m hm => ⟨⟨m, hm⟩, rfl⟩⟩

Premises used: Exists.intro, CanLift.mk, Finset.mk, rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Multiset α
nodup : s.Nodup
t : Multiset α
nodup_1 : t.Nodup
h : { val := s, nodup := nodup : Finset α }.val = { val := t, nodup := nodup_1 }.val
refl : ∀ (nodup_2 : s.Nodup), { val := s, nodup := nodup : Finset α } = { val := s, nodup := nodup_2 }
⊢ { val := s, nodup := nodup : Finset α } = { val := t, nodup := nodup_1 }

Tactic:
cases h
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Multiset α
nodup nodup_1 : s.Nodup
⊢ { val := s, nodup := nodup : Finset α } = { val := s, nodup := nodup_1 }

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Finset α) val

Tactic:
fun _ _ => eq_of_veq

Premises used: Finset.eq_of_veq, Function.Injective
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s t : Finset α
⊢ s.val = t.val ↔ s = t

Tactic:
val_injective.eq_iff

Premises used: Function.Injective.eq_iff, Finset.val_injective
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
a : α
s : Finset α
⊢ a ∈ s ↔ a ∈ s.val

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Multiset.Mem
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
a : α
s : Finset α
⊢ (a ∈ s.val) = (a ∈ s)

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
a : α
s : Multiset α
nd : s.Nodup
⊢ a ∈ { val := s, nodup := nd : Finset α } ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Multiset.Mem
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬a = b) ↔ ¬a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬b = a) ↔ ¬a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
a : α
s : Finset α
⊢ a ∈ (↑s : Set α) ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_4
s : Finset α
⊢ {a : α | a ∈ s} = (↑s : Set α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
x : (↑(↑s : Set α) : Type u_1)
⊢ (↑x : α) ∈ s

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s : Finset α
x : (↑(↑s : Set α) : Type u_1)
h : (↑x : α) ∈ (↑s : Set α)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ (↑s : Set α)) (↑x : α) h = x

Tactic:
Subtype.coe_eta _ _

Premises used: Subtype.coe_eta
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
⊢ s₁ = s₂

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_1
s₁ s₂ : Finset α
⊢ (↑s₁ : Set α) = (↑s₂ : Set α) ↔ s₁ = s₂

Tactic:
SetLike.coe_set_eq

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_4
⊢ Injective (α := Finset α) SetLike.coe

Tactic:
fun _s _t => coe_inj.1

Premises used: Finset.coe_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_4
s : Finset α
p : ↥s → Prop
⊢ (∀ (x : ↥s), p x) ↔ ∀ (x : α) (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)

Tactic:
Subtype.forall

Premises used: Subtype.forall
-- Module: Mathlib.Data.Finset.Defs
Goal:
α : Type u_4
s : Finset α
p : ↥s → Prop
⊢ (∃ (x : ↥s), p x) ↔ ∃ (x : α), ∃ (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)

Tactic:
Subtype.exists

Premises used: Subtype.exists
-- Module: Mathlib.Data.Finset.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
α : ι → Type u_5
_ne : ∀ (i : ι), Nonempty.{u_5 + 1} (α i)
s : Finset ι
⊢ CanLift ((i : ↥s) → α (↑i : ι)) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : ↥s) ↦ f (↑i : ι))
    fun (x : (i : ↥s) → α (↑i : ι)) ↦ True

Tactic:
PiSubtype.canLift ι α (· ∈ s)

Premises used: Membership.mem, PiSubtype.canLift