awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have ht₁ : s = t
Tactic: rw [ndinsert_of_mem h] at ht
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht_1 : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have pos : ∀ (ht : ndinsert a s = s),
  s.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a sorry)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) sorry) s.attach)
Tactic: subst ht
Cleared hypotheses: t, ht_1, ht
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) s.attach)
have pos : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a sorry) (map id s.attach)
Tactic: rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
h : a ∈ s
ht : ndinsert a s = s
pos : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯) (map id s.attach)
⊢ s.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) s.attach)
have pos₁ : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a sorry) s.attach
Tactic: rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
h : a ∈ s
ht : ndinsert a s = s
pos : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯) (map id s.attach)
pos₁ : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯) s.attach
⊢ s.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) s.attach)
have pos₂ : s.attach = s.attach
Tactic: rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have ht₁ : a ::ₘ s = t
Tactic: rw [ndinsert_of_notMem h] at ht
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht_1 : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have neg : ∀ (ht : ndinsert a s = a ::ₘ s),
  (a ::ₘ s).attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) a sorry)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) (↑p : α) sorry) s.attach)
Tactic: subst ht
Cleared hypotheses: t, ht_1, ht
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have rw : ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: rw [_root_.disjoint_comm, disjoint_ndinsert_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₁ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₁ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₅ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
mp₅ mp₆ mp₇ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₅ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ s.ndunion t = s.dedup + t
have h₁ : ∀ (a b : List α)
  (h :
    _root_.Disjoint (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
  ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) + Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b
Tactic: induction s, t using Quot.induction_on₂
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndunion t = t
have h₁ : ∀ (a b : List α)
  (h :
    Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
  ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b
Tactic: induction s, t using Quot.induction_on₂
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁ : Multiset α).ndinter (↑l₂ : Multiset α) = (↑(l₁ ∩ l₂) : Multiset α)
have simp : List.filter (fun (b : α) ↦ elem b l₂) l₁ ~ l₁ ∩ l₂
Tactic: simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup
have rw : (s.ndinter t).Nodup
Tactic: rw [← ndinter_eq_inter d]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t
have rw : s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t
Tactic: rw [← subset_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndinter t = s
have h₁ : ∀ (a b : List α)
  (h :
    Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
  ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
Tactic: induction s, t using Quot.induction_on₂
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
have h₁ : (↑a : Multiset α).ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) = (↑a : Multiset α)
Tactic: rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
h₁ : (↑a : Multiset α).ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) = (↑a : Multiset α)
⊢ ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
have h₂ : (↑a : Multiset α).ndinter (↑b : Multiset α) = (↑a : Multiset α)
Tactic: rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
h₁ : (↑a : Multiset α).ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) = (↑a : Multiset α)
h₂ : (↑a : Multiset α).ndinter (↑b : Multiset α) = (↑a : Multiset α)
⊢ ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
have h₃ : (↑(a ∩ b) : Multiset α) = (↑a : Multiset α)
Tactic: rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
h₁ : (↑a : Multiset α).ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) = (↑a : Multiset α)
h₂ : (↑a : Multiset α).ndinter (↑b : Multiset α) = (↑a : Multiset α)
h₃ : (↑(a ∩ b) : Multiset α) = (↑a : Multiset α)
⊢ ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
have h₄ : (↑a : Multiset α) = (↑a : Multiset α)
Tactic: rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : m.ToType
⊢ 0 < count (x.fst (β := fun (x : α) ↦ Fin (count x m))) m
have this : (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) < count (x.fst (β := fun (x : α) ↦ Fin (count x m))) m
Tactic: have := x.2.2
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ Membership.mem (γ := Finset (α × ℕ))
      (m.toFinset.disjiUnion (fun (x : α) ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) ⋯)
      (x, i) ↔
    Membership.mem (γ := Set (α × ℕ)) {p : α × ℕ | p.2 < count p.1 m} (x, i)
have simp_rw : (∃ a ∈ m, ∃ a_1 < count a m, a = x ∧ a_1 = i) ↔ i < count x m
Tactic: simp_rw [Finset.mem_disjiUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range,
        Function.Embedding.coeFn_mk, Prod.mk_inj, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m, ∃ a_1 < count a m, a = x ∧ a_1 = i) ↔ i < count x m
have simp : i < count x m → x ∈ m
Tactic: simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m
have a : ∀ (a : α), count a (map Prod.fst m.toEnumFinset.val) = count a m
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset
have rw : (map Prod.fst m.toEnumFinset.val).toFinset = m.toFinset
Tactic: rw [Finset.image, Multiset.map_toEnumFinset_fst]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
rw : (map Prod.fst m.toEnumFinset.val).toFinset = m.toFinset
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset
have rw₁ : m.toFinset = m.toFinset
Tactic: rw [Finset.image, Multiset.map_toEnumFinset_fst]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ map Prod.fst s.val ≤ m
have simp_rw : ∀ (a : α), (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
Tactic: simp_rw [le_iff_count, count_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
have inl : ∀ (ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card = 0),
  (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
Tactic: obtain ha | ha := (s.1.filter fun x ↦ a = x.1).card.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
inl :
  ∀ (ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card = 0),
    (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
have inr : ∀ (ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card > 0),
  (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
Tactic: obtain ha | ha := (s.1.filter fun x ↦ a = x.1).card.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card = 0
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
have inl : 0 ≤ count a m
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card > 0
⊢ ∃ n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1, (a, n) ∈ s
have by_contra! : ∀ (h : ∀ (n : ℕ) (_ : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1), (a, n) ∉ s), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card > 0
h : ∀ (n : ℕ) (_ : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1), (a, n) ∉ s
⊢ False
have h₁ : {x ∈ s | x.1 = a} ⊆ SProd.sprod (α := Finset α) {a} (Finset.range ((filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1))
Tactic: replace h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
      simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card > 0
h :
  {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {a} (Finset.range ((filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1))
⊢ False
have this : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card ≤ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1
Tactic: have : card (s.1.filter fun x ↦ a = x.1) ≤ card (s.1.filter fun x ↦ a = x.1) - 1 := by
      simpa [Finset.card, eq_comm] using Finset.card_mono h
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card > 0
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
have inr : ∀ (n : ℕ) (han : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1) (hn : (a, n) ∈ s),
  (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
Tactic: obtain ⟨n, han, hn⟩ : ∃ n ≥ card (s.1.filter fun x ↦ a = x.1) - 1, (a, n) ∈ s := by
    by_contra! h
    replace h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
      simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h
    have : card (s.1.filter fun x ↦ a = x.1) ≤ card (s.1.filter fun x ↦ a = x.1) - 1 := by
      simpa [Finset.card, eq_comm] using Finset.card_mono h
    lia
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset
have simp : p.2 < count p.1 m₁ → p.2 < count p.1 m₂
Tactic: simp only [Multiset.mem_toEnumFinset]