awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
simp_rw₂ :
  Eq (α := ℕ)
    (∏
      i ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      #(uIcc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
          ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
    (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
have simp_rw₃ : Eq (α := ℕ)
  (∏
    x ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    ((HSub.hSub (α := ℤ) (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)
          (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)).natAbs +
      1))
  (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
Tactic: simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
simp_rw₂ :
  Eq (α := ℕ)
    (∏
      i ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      #(uIcc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
          ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
    (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
simp_rw₃ :
  Eq (α := ℕ)
    (∏
      x ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      ((HSub.hSub (α := ℤ)
            (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)
            (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)).natAbs +
        1))
    (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
have simp_rw₄ : Eq (α := ℕ)
  (∏
    x ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    ((HSub.hSub (α := ℤ) (↑(count x t) : ℤ) (↑(count x s) : ℤ)).natAbs + 1))
  (∏ x ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count x t) : ℤ) (↑(count x s) : ℤ)).natAbs + 1))
Tactic: simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw₁ : Eq (α := ℕ) (∏ i ∈ toFinset ⊥ ∪ s.toFinset, (count i s + 1 - count i ⊥)) (∏ i ∈ s.toFinset, (count i s + 1))
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
simp_rw₁ : Eq (α := ℕ) (∏ i ∈ toFinset ⊥ ∪ s.toFinset, (count i s + 1 - count i ⊥)) (∏ i ∈ s.toFinset, (count i s + 1))
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw₂ : Eq (α := ℕ) (∏ x ∈ toFinset 0 ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
simp_rw₁ : Eq (α := ℕ) (∏ i ∈ toFinset ⊥ ∪ s.toFinset, (count i s + 1 - count i ⊥)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₂ : Eq (α := ℕ) (∏ x ∈ toFinset 0 ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw₃ : Eq (α := ℕ) (∏ x ∈ ∅ ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
simp_rw₁ : Eq (α := ℕ) (∏ i ∈ toFinset ⊥ ∪ s.toFinset, (count i s + 1 - count i ⊥)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₂ : Eq (α := ℕ) (∏ x ∈ toFinset 0 ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₃ : Eq (α := ℕ) (∏ x ∈ ∅ ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw₄ : Eq (α := ℕ) (∏ x ∈ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
simp_rw₁ : Eq (α := ℕ) (∏ i ∈ toFinset ⊥ ∪ s.toFinset, (count i s + 1 - count i ⊥)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₂ : Eq (α := ℕ) (∏ x ∈ toFinset 0 ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₃ : Eq (α := ℕ) (∏ x ∈ ∅ ∪ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
simp_rw₄ : Eq (α := ℕ) (∏ x ∈ s.toFinset, (count x s + 1 - count x 0)) (∏ i ∈ s.toFinset, (count i s + 1))
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)
have simp_rw₅ : Eq (α := ℕ) (∏ x ∈ s.toFinset, (count x s + 1 - 0)) (∏ i ∈ s.toFinset, (count i s + 1))
Tactic: simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Lattice (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup
have rw : ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Lattice (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup
have rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
Tactic: rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Lattice (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).sup = a ⊔ s.sup
have rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
Tactic: rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Lattice (goal)
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset (Multiset α)
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup
have empty : Nodup.{u_2} (α := α) (sup 0) ↔ ∀ (a : Multiset α), Membership.mem (γ := Multiset (Multiset α)) 0 a → a.Nodup
Tactic: induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.Lattice (goal)
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset (Multiset α)
empty : Nodup.{u_2} (α := α) (sup 0) ↔ ∀ (a : Multiset α), Membership.mem (γ := Multiset (Multiset α)) 0 a → a.Nodup
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup
have cons : ∀ (a : Multiset α) (s : Multiset (Multiset α)) (h : s.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ s → a.Nodup),
  (a ::ₘ s).sup.Nodup ↔ ∀ (a_1 : Multiset α), a_1 ∈ a ::ₘ s → a_1.Nodup
Tactic: induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
have h₁ : ∀ (a : List α)
  (h : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) x → f x = g x),
  map f (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) =
    map g (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → β
f' : α → β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m
have subst : ∀ {f' : α → β} (hf : ∀ (a : α), a ∈ m → f a ≍ f' a), map f m ≍ map f' m
Tactic: subst h
Cleared hypotheses: β', f', h, hf
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (hypothesis)
Goal:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m
have hf₁ : ∀ (a : α), a ∈ m → f a = f' a
Tactic: simp at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f
have h : ∀ (x : Multiset α), (map f ∘ cons t) x = (cons (f t) ∘ map f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst : CanLift α β c p
x : Multiset α
l : List α
hl : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x
⊢ ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l
have mk : ∀ (l : List β), ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (List.map c l)
Tactic: lift l to List β using hl
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0
have rw : (map f s).card = 0 ↔ s = 0
Tactic: rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : (map f s).card = 0 ↔ s = 0
⊢ map f s = 0 ↔ s = 0
have rw₁ : s.card = 0 ↔ s = 0
Tactic: rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : (map f s).card = 0 ↔ s = 0
rw₁ : s.card = 0 ↔ s = 0
⊢ map f s = 0 ↔ s = 0
have rw₂ : s = 0 ↔ s = 0
Tactic: rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f s ↔ s = 0
have rw : map f s = 0 ↔ s = 0
Tactic: rw [eq_comm, map_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : map f s = 0 ↔ s = 0
⊢ 0 = map f s ↔ s = 0
have rw₁ : s = 0 ↔ s = 0
Tactic: rw [eq_comm, map_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b
have mp : map f s = {b} → ∃ (a : α), s = {a} ∧ f a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
mp : map f s = {b} → ∃ (a : α), s = {a} ∧ f a = b
⊢ map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b
have mpr : (∃ (a : α), s = {a} ∧ f a = b) → map f s = {b}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ (a : α), s = {a}
have rw : s.card = 1
Tactic: rw [← card_eq_one, ← card_map, h, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
rw : s.card = 1
⊢ ∃ (a : α), s = {a}
have rw₁ : (map f s).card = 1
Tactic: rw [← card_eq_one, ← card_map, h, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
rw : s.card = 1
rw₁ : (map f s).card = 1
f₁ : α → β
rw₂ : Type v
⊢ ∃ (a : α), s = {a}
have rw₃ : card (α := β) {b} = 1
Tactic: rw [← card_eq_one, ← card_map, h, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
rw : s.card = 1
rw₁ : (map f s).card = 1
f₁ : α → β
rw₂ : Type v
rw₃ : card (α := β) {b} = 1
⊢ ∃ (a : α), s = {a}
have rw₄ : Eq (α := ℕ) 1 1
Tactic: rw [← card_eq_one, ← card_map, h, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ (a : α), s = {a} ∧ f a = b
have mp : ∀ (a : α) (ha : s = {a}), ∃ (a : α), s = {a} ∧ f a = b
Tactic: obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ (a : α), s = {a} ∧ f a = b
have mp : f a = b
Tactic: refine ⟨a, ha, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b
have mp : Membership.mem (γ := Multiset β) {b} (f a)
Tactic: rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
mp : Membership.mem (γ := Multiset β) {b} (f a)
⊢ f a = b
have mp₁ : f a ∈ map f s
Tactic: rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
mp : Membership.mem (γ := Multiset β) {b} (f a)
mp₁ : f a ∈ map f s
⊢ f a = b
have mp₂ : f a ∈ map f {a}
Tactic: rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
mp : Membership.mem (γ := Multiset β) {b} (f a)
mp₁ : f a ∈ map f s
mp₂ : f a ∈ map f {a}
⊢ f a = b
have mp₃ : Membership.mem (γ := Multiset β) {f a} (f a)
Tactic: rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
mp : Membership.mem (γ := Multiset β) {b} (f a)
mp₁ : f a ∈ map f s
mp₂ : f a ∈ map f {a}
mp₃ : Membership.mem (γ := Multiset β) {f a} (f a)
⊢ f a = b
have mp₄ : f a = f a
Tactic: rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t
have mp : (∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) → map f s = b ::ₘ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
mp : (∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) → map f s = b ::ₘ t
⊢ (∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t
have mpr : map f s = b ::ₘ t → ∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (s.erase a)
have mp : map f s = map f (a ::ₘ s.erase a)
Tactic: rw [← map_cons, Multiset.cons_erase ha]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
mp : map f s = map f (a ::ₘ s.erase a)
⊢ map f s = f a ::ₘ map f (s.erase a)
have mp₁ : map f s = map f s
Tactic: rw [← map_cons, Multiset.cons_erase ha]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s
have rw : b ∈ b ::ₘ t
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (hypothesis)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
have this : b ∈ map f s
Tactic: have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
have mpr : ∀ (a : α) (h1 : a ∈ s) (h : map f s = f a ::ₘ t) (this : f a ∈ map f s),
  ∃ (a_1 : α), a_1 ∈ s ∧ f a_1 = f a ∧ map f (s.erase a_1) = t
Tactic: obtain ⟨a, h1, rfl⟩ := mem_map.mp this
Cleared hypotheses: b, h, this
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ (a_1 : α), a_1 ∈ s ∧ f a_1 = f a ∧ map f (s.erase a_1) = t
have mpr : ∀ (u : Multiset α) (h1 : a ∈ a ::ₘ u) (h : map f (a ::ₘ u) = f a ::ₘ t) (this : f a ∈ map f (a ::ₘ u)),
  ∃ (a_1 : α), a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t
Tactic: obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
Cleared hypotheses: s, h1, h, this
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (hypothesis)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ (a_1 : α), a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t
have h₁ : map f u = t
Tactic: rw [map_cons, cons_inj_right] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ (a_1 : α), a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t
have mpr : map f ((a ::ₘ u).erase a) = t
Tactic: refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
mpr : map f u = t
⊢ map f ((a ::ₘ u).erase a) = t
have mpr₁ : t = t
Tactic: rw [Multiset.erase_cons_head, h]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) (↑l : Multiset α)
⊢ b₁ ∈ replicate (↑l : Multiset α).card b₂
have rwa : ∀ (h : b₁ ∈ replicate (↑l : Multiset α).card b₂), b₁ ∈ replicate (↑l : Multiset α).card b₂
Tactic: rwa [map_const] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t
have refine : ∀ (H : map f t ≤ map f s), t.card ≤ s.card
Tactic: refine (map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card
have rw : (map f t).card ≤ (map f s).card
Tactic: rw [← s.card_map f, ← t.card_map f]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
⊢ map f (s.erase x) = (map f s).erase (f x)
have cons : ∀ (y : α) (s : Multiset α) (ih : map f (s.erase x) = (map f s).erase (f x)),
  map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Tactic: induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have pos : ∀ (hxy : y = x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Tactic: by_cases hxy : y = x
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
pos : ∀ (hxy : y = x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg : ∀ (hxy : ¬y = x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Tactic: by_cases hxy : y = x