awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
empty : a ∈ inf ∅ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a ∈ f i
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
    (a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i) → (a ∈ (Finset.cons a_1 s h).inf f ↔ ∀ i ∈ Finset.cons a_1 s h, a ∈ f i)
⊢ a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
f : ι → Finset α
a : α
⊢ a ∈ inf ∅ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
f : ι → Finset α
a : α
a_1 : ι
s : Finset ι
h : a_1 ∉ s
h_1 : a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
⊢ a ∈ (cons a_1 s h).inf f ↔ ∀ i ∈ cons a_1 s h, a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
intro : ∀ (val : Fintype α), ∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀
⊢ ∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
val : Fintype α
⊢ ∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀

Tactic:
simpa using exists_max_image univ f univ_nonempty

Premises used: Finset.univ, Finset.univ_nonempty, Finset.exists_max_image
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
intro : ∀ (val : Fintype α), ∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x
⊢ ∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
val : Fintype α
⊢ ∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x

Tactic:
simpa using exists_min_image univ f univ_nonempty

Premises used: Finset.univ, Finset.univ_nonempty, Finset.exists_min_image
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ (↑l.permutations : Multiset (List α)) = (↑l'.permutations : Multiset (List α))

Tactic:
coe_eq_coe.mpr ?_

Premises used: Iff.mpr, Multiset.coe_eq_coe
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
refine : l.permutations ~ l'.permutations
⊢ (↑l.permutations : Multiset (List α)) = (↑l'.permutations : Multiset (List α))

Tactic:
refine coe_eq_coe.mpr ?_

Premises used: Iff.mpr, Multiset.coe_eq_coe
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ l.permutations ~ l'.permutations

Tactic:
Perm.permutations h

Premises used: List.Perm.permutations
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ l.permutations ~ l'.permutations

Tactic:
exact Perm.permutations h

Premises used: List.Perm.permutations
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).lists = (↑l.permutations : Multiset (List α))

Tactic:
rfl

Premises used: Multiset.lists, rfl
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : Finset α
⊢ l.val.Nodup

Tactic:
have h_nodup : l.val.Nodup := l.nodup
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.toList.Nodup

Tactic:
rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup

Premises used: Multiset.coe_nodup, Finset.coe_toList
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
rw : (↑l.toList : Multiset α).lists.Nodup
⊢ l.val.lists.Nodup

Tactic:
rw [← Finset.coe_toList l]

Premises used: Finset.coe_toList
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ (↑l.toList : Multiset α).lists.Nodup

Tactic:
nodup_permutations l.val.toList (h_nodup)

Premises used: Multiset.Nodup, List.nodup_permutations, Multiset.toList, Finset.toList, Finset.val
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ (↑l.toList : Multiset α).lists.Nodup

Tactic:
exact nodup_permutations l.val.toList (h_nodup)

Premises used: List.nodup_permutations, Multiset.toList, Finset.val
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
s : Multiset α
l : List α
h : ∀ (a : List α), l ∈ lists ⟦a⟧ ↔ ⟦a⟧ = ⟦l⟧
⊢ l ∈ s.lists ↔ s = ⟦l⟧

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
l a : List α
⊢ l ∈ lists ⟦a⟧ ↔ ⟦a⟧ = ⟦l⟧

Tactic:
simpa using perm_comm

Premises used: List.perm_comm
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
refine_1 : Finset (List α)
refine_2 :
  ∀ (x : List α),
    Membership.mem (γ := Finset (List α))
        (let univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ);
        let allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists;
        { val := allPerms, nodup := ⋯ })
        x ↔
      x.Nodup
⊢ Fintype { l : List α // l.Nodup }

Tactic:
refine Fintype.subtype ?_ ?_

Premises used: Fintype.subtype
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
refine_1 :
  (∀ a ∈ univSubsets, a.val.lists.Nodup) ∧
    Multiset.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
      univSubsets
⊢ Finset (List α)

Tactic:
refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
refine_1 :
  Multiset.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
    univSubsets
⊢ (∀ a ∈ univSubsets, a.val.lists.Nodup) ∧
    Multiset.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
      univSubsets

Tactic:
simp only [Multiset.lists_nodup_finset, implies_true, true_and]

Premises used: Multiset.lists_nodup_finset, implies_true, true_and
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
h :
  univSubsets = (↑(Finset.toList (Finset.powerset Finset.univ)) : Multiset (Finset α)) ∧
    List.Pairwise.{u_1} (α := Finset α)
      (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
      (Finset.toList (Finset.powerset Finset.univ))
⊢ ∃ (l : List (Finset α)),
    univSubsets = (↑l : Multiset (Finset α)) ∧
      List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l

Tactic:
use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))

Premises used: Finset.univ, Finset.toList, Finset.powerset
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
h : univSubsets = (↑(Finset.toList (Finset.powerset Finset.univ)) : Multiset (Finset α))
h₁ :
  List.Pairwise.{u_1} (α := Finset α)
    (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
    (Finset.toList (Finset.powerset Finset.univ))
⊢ univSubsets = (↑(Finset.toList (Finset.powerset Finset.univ)) : Multiset (Finset α)) ∧
    List.Pairwise.{u_1} (α := Finset α)
      (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
      (Finset.toList (Finset.powerset Finset.univ))

Tactic:
constructor
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
h : univSubsets = Finset.val (Finset.powerset Finset.univ)
⊢ univSubsets = (↑(Finset.toList (Finset.powerset Finset.univ)) : Multiset (Finset α))

Tactic:
simp only [Finset.coe_toList]

Premises used: Finset.coe_toList
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
⊢ univSubsets = Finset.val (Finset.powerset Finset.univ)

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
⊢ Nodup.{u_1} (α := Finset α) (Finset.toList (Finset.powerset Finset.univ))

Tactic:
Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))

Premises used: Finset.univ, Finset.nodup_toList, Finset.powerset
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
h :
  Eq.{u_1 + 1} (α := List (Finset α) → Prop)
    (List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)) Nodup
⊢ List.Pairwise.{u_1} (α := Finset α)
    (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
    (Finset.toList (Finset.powerset Finset.univ))

Tactic:
convert! Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))

Premises used: Finset.univ, Finset.nodup_toList, Finset.powerset
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
h :
  ∀ (l : List (Finset α)),
    List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l ↔ l.Nodup
⊢ Eq.{u_1 + 1} (α := List (Finset α) → Prop)
    (List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)) Nodup

Tactic:
ext l
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
⊢ List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l ↔
    List.Pairwise (fun (x1 x2 : Finset α) ↦ x1 ≠ x2) l

Tactic:
Pairwise.iff ?_

Premises used: List.Pairwise.iff
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
h :
  ∀ (a b : Finset α),
    Function.onFun (β := Multiset (List α)) _root_.Disjoint (fun (s : Finset α) ↦ s.val.lists) a b ↔ a ≠ b
⊢ List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l ↔
    List.Pairwise (fun (x1 x2 : Finset α) ↦ x1 ≠ x2) l

Tactic:
refine Pairwise.iff ?_

Premises used: List.Pairwise.iff
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
h :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m ≠ n
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ m.val.lists → x ≤ n.val.lists → x ≤ ⊥) ↔ m ≠ n

Tactic:
rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]

Premises used: Multiset.lists_coe, Finset.coe_toList
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
⊢ _root_.Disjoint (↑m.toList.permutations : Multiset (List α)) (↑n.toList.permutations : Multiset (List α)) ↔
    m.toList.permutations.Disjoint n.toList.permutations

Tactic:
have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  _root_.Disjoint (↑m.toList.permutations : Multiset (List α)) (↑n.toList.permutations : Multiset (List α)) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations

Tactic:
rw [_root_.Disjoint] at this

Premises used: Disjoint
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : m.toList.permutations.Disjoint n.toList.permutations ↔ m ≠ n
⊢ (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m ≠ n

Tactic:
rw [this]
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n
⊢ m.toList.permutations.Disjoint n.toList.permutations ↔ ¬m = n

Tactic:
rw [List.disjoint_iff_ne]

Premises used: List.disjoint_iff_ne
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n
h₁ : ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n

Tactic:
constructor
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
h₁ : ∀ (hc : m = n), False
⊢ ¬m = n

Tactic:
by_contra hc
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
⊢ ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
rw [hc] at h
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
h₁ : ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
⊢ m = n

Tactic:
rw [hc] at h
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
h₁ : ∀ (h : True), ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b
⊢ False

Tactic:
contrapose! h
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
hc : m = n
h : True
h₁ : n.toList ∈ n.toList.permutations ∧ ∃ b ∈ n.toList.permutations, n.toList = b
⊢ ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b

Tactic:
use n.toList

Premises used: Finset.toList
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
hc : m = n
h : True
⊢ n.toList ∈ n.toList.permutations ∧ ∃ b ∈ n.toList.permutations, n.toList = b

Tactic:
simp
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
h₁ : ∀ (a : List α), a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b
⊢ ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
simp only [mem_permutations]

Premises used: List.mem_permutations
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
h₁ : ∀ (hab : a = b), False
⊢ a ≠ b

Tactic:
by_contra hab
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
h₁ : m = n
⊢ False

Tactic:
absurd h
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
⊢ b ~ m.toList

Tactic:
rw [hab] at ha
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
ha₁ : b ~ m.toList
⊢ b ~ n.toList

Tactic:
rw [hab] at ha
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
ha₁ : b ~ m.toList
hb₁ : b ~ n.toList
⊢ a = b

Tactic:
rw [hab] at ha
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a b : List α
ha : b ~ m.toList
hb : b ~ n.toList
hab : a = b
⊢ m = n

Tactic:
Finset.perm_toList.mp <| Perm.trans ha.symm hb

Premises used: List.Perm.trans, Finset.perm_toList, Iff.mp, List.Perm.symm