awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ (↑l.permutations : Multiset (List α)) = (↑l'.permutations : Multiset (List α))
have refine : l.permutations ~ l'.permutations
Tactic: refine coe_eq_coe.mpr ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
Goal:
α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup
have h_nodup : l.val.Nodup
Tactic: have h_nodup : l.val.Nodup := l.nodup
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
Goal:
α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup
have h_nodup₁ : l.toList.Nodup
Tactic: rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup
Cleared hypotheses: h_nodup
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup
have rw : (↑l.toList : Multiset α).lists.Nodup
Tactic: rw [← Finset.coe_toList l]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ l ∈ s.lists ↔ s = ⟦l⟧
have h : ∀ (a : List α), l ∈ lists ⟦a⟧ ↔ ⟦a⟧ = ⟦l⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ Fintype { l : List α // l.Nodup }
have refine_1 : Finset (List α)
Tactic: refine Fintype.subtype ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
refine_1 : Finset (List α)
⊢ Fintype { l : List α // l.Nodup }
have 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 := sorry })
      x ↔
    x.Nodup
Tactic: refine Fintype.subtype ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ Finset (List α)
have refine_1 : (∀ a ∈ univSubsets, a.val.lists.Nodup) ∧
  Multiset.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
    univSubsets
Tactic: refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ (∀ a ∈ univSubsets, a.val.lists.Nodup) ∧
    Multiset.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
      univSubsets
have refine_1 : 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]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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 α)),
    univSubsets = (↑l : Multiset (Finset α)) ∧
      List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l
have 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))
Tactic: use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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.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))
have h : univSubsets = (↑(Finset.toList (Finset.powerset Finset.univ)) : Multiset (Finset α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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 α))
⊢ 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))
have h₁ : 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
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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.toList (Finset.powerset Finset.univ)) : Multiset (Finset α))
have h : univSubsets = Finset.val (Finset.powerset Finset.univ)
Tactic: simp only [Finset.coe_toList]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ List.Pairwise.{u_1} (α := Finset α)
    (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)
    (Finset.toList (Finset.powerset Finset.univ))
have h : Eq.{u_1 + 1} (α := List (Finset α) → Prop)
  (List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)) Nodup
Tactic: convert! Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ Eq.{u_1 + 1} (α := List (Finset α) → Prop)
    (List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists)) Nodup
have h : ∀ (l : List (Finset α)),
  List.Pairwise (Function.onFun (β := Multiset (List α)) _root_.Disjoint fun (s : Finset α) ↦ s.val.lists) l ↔ l.Nodup
Tactic: ext l
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
have h : ∀ (a b : Finset α),
  Function.onFun (β := Multiset (List α)) _root_.Disjoint (fun (s : Finset α) ↦ s.val.lists) a b ↔ a ≠ b
Tactic: refine Pairwise.iff ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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 α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ m.val.lists → x ≤ n.val.lists → x ≤ ⊥) ↔ m ≠ n
have h : (∀ ⦃x : Multiset (List α)⦄,
    x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
  m ≠ n
Tactic: rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
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 α
⊢ (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m ≠ n
have this : _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
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
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 ≠ n
have this₁ : (∀ ⦃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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m ≠ n
have h : m.toList.permutations.Disjoint n.toList.permutations ↔ m ≠ n
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ m.toList.permutations.Disjoint n.toList.permutations ↔ ¬m = n
have h : (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n
Tactic: rw [List.disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n
have h : (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n
have h₁ : ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
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
⊢ False
have h₁ : ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
Tactic: rw [hc] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ False
have h₁ : ∀ (h : True), ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b
have h₁ : n.toList ∈ n.toList.permutations ∧ ∃ b ∈ n.toList.permutations, n.toList = b
Tactic: use n.toList
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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 ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
have h₁ : ∀ (a : List α), a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b
Tactic: simp only [mem_permutations]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
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
⊢ False
have h₁ : m = n
Tactic: absurd h
-- Lean 4 proof step from Mathlib.Data.Fintype.List (hypothesis)
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
⊢ m = n
have ha₁ : b ~ m.toList
Tactic: rw [hab] at ha
Cleared hypotheses: ha, hb, hab
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : 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 := ⋯ })
      l ↔
    l.Nodup
have refine_2 : (∃ (a : Finset α), a.val = (↑l : Multiset α)) ↔ l.Nodup
Tactic: simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset,
      Finset.subset_univ, Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : List α
⊢ (∃ (a : Finset α), a.val = (↑l : Multiset α)) ↔ l.Nodup
have refine_2 : (∃ (a : Finset α), a.val = (↑l : Multiset α)) → l.Nodup
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : List α
refine_2 : (∃ (a : Finset α), a.val = (↑l : Multiset α)) → l.Nodup
⊢ (∃ (a : Finset α), a.val = (↑l : Multiset α)) ↔ l.Nodup
have refine_2₁ : l.Nodup → ∃ (a : Finset α), a.val = (↑l : Multiset α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : List α
h : ∃ (a : Finset α), a.val = (↑l : Multiset α)
⊢ l.Nodup
have refine_2 : ∀ (f : Finset α) (hf : f.val = (↑l : Multiset α)), l.Nodup
Tactic: rcases h with ⟨f, hf⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
⊢ l.Nodup
have a : l.Nodup ↔ f.val.Nodup
Tactic: convert! f.nodup
-- Lean 4 proof step from Mathlib.Data.Fintype.List (goal)
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
⊢ l.Nodup ↔ f.val.Nodup
have a : l.Nodup ↔ (↑l : Multiset α).Nodup
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
⊢ Trunc (P α)
have apply : P (ULift.{u, 0} (Fin (card α))) → Trunc (P α)
Tactic: apply Trunc.bind (this (Fintype.card α))
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
⊢ Trunc (P α)
have apply : α ≃ Fin (card α) → P α
Tactic: apply Trunc.map _ (Fintype.truncEquivFin α)
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
⊢ Trunc (P α)
have suffices : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
Tactic: suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n)) by
    apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))
have this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
Tactic: have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))
have zero : PEmpty.{u + 1} ≃ ULift.{u, 0} (Fin 0) → Trunc (P (ULift.{u, 0} (Fin 0)))
Tactic: apply Trunc.bind (truncEquivOfCardEq this)
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
e : PEmpty.{u + 1} ≃ ULift.{u, 0} (Fin 0)
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))
have zero : P (ULift.{u, 0} (Fin 0))
Tactic: apply Trunc.mk
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))
have this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
Tactic: have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))
have succ : Option (ULift.{u, 0} (Fin n)) ≃ ULift.{u, 0} (Fin n.succ) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))
Tactic: apply Trunc.bind (truncEquivOfCardEq this)
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
e : Option (ULift.{u, 0} (Fin n)) ≃ ULift.{u, 0} (Fin n.succ)
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))
have apply : P (ULift.{u, 0} (Fin n)) → P (ULift.{u, 0} (Fin (n + 1)))
Tactic: apply Trunc.map _ ih