awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Interval
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))
simp_rw₅ : Eq (α := ℕ) (∏ x ∈ s.toFinset, (count x s + 1 - 0)) (∏ i ∈ s.toFinset, (count i s + 1))
⊢ #(Finset.Iic 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]

Premises used: Finset.empty_union, Finset.Iic_eq_Icc, Multiset.bot_eq_zero, Multiset.count_zero, tsub_zero, Multiset.toFinset_zero, Multiset.card_Icc
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
l : List α
⊢ (↑l : Multiset α).sup = List.foldr (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ l

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.sup, rfl, Multiset.fold
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := α) (sup 0) ⊥

Tactic:
fold_zero _ _

Premises used: Multiset.fold_zero, Multiset.sup
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a : α
s : Multiset α
⊢ (a ::ₘ s).sup = a ⊔ s.sup

Tactic:
fold_cons_left _ _ _ _

Premises used: Multiset.fold_cons_left, Multiset.sup
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a : α
⊢ sup {a} = a

Tactic:
sup_bot_eq _

Premises used: Multiset.foldr, sup_bot_eq, Multiset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).sup = fold (fun (x1 x2 : α) ↦ x1 ⊔ x2) (⊥ ⊔ ⊥) (s₁ + s₂)

Tactic:
simp [sup]

Premises used: Multiset.sup
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), Membership.mem (γ := Multiset α) 0 b → b ≤ a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.sup ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)

Tactic:
simp +contextual [or_imp, forall_and]

Premises used: or_imp, forall_and
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Multiset α
a : α
h : a ∈ s
⊢ a ≤ s.sup

Tactic:
sup_le.1 le_rfl _ h

Premises used: le_rfl, Iff.mp, Multiset.sup_le
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Multiset α
h : s₁ ⊆ s₂
⊢ s₁.sup ≤ s₂.sup

Tactic:
sup_le.2 fun _ hb => le_sup (h hb)

Premises used: Iff.mpr, Multiset.le_sup, Multiset.sup_le
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Multiset α
⊢ s.dedup.sup = s.sup

Tactic:
fold_dedup_idem _ _ _

Premises used: Multiset.fold_dedup_idem, Multiset.sup
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
rw : ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.sup_dedup, Multiset.sup_add
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
rw : ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.sup_dedup, Multiset.sup_add
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a : α
s : Multiset α
rw : ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
⊢ (ndinsert a s).sup = a ⊔ s.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]

Premises used: Multiset.dedup_ext, Iff.mpr, Multiset.sup_cons, Multiset.sup_dedup
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_2
inst : DecidableEq α
⊢ Nodup.{u_2} (α := α) (sup 0) ↔ ∀ (a : Multiset α), Membership.mem (γ := Multiset (Multiset α)) 0 a → a.Nodup

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Lattice
Goal:
α : Type u_2
inst : DecidableEq α
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:
simp [h]
-- Module: Mathlib.Data.Multiset.Lattice
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
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
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup

Tactic:
induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
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)
⊢ map f s = map g s

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f g : α → β
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:
congr_arg _ (List.map_congr_left h)

Premises used: Multiset.map, List.map_congr_left, congr_arg, Multiset.ofList
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f g : α → β
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:
exact congr_arg _ (List.map_congr_left h)

Premises used: List.map_congr_left, congr_arg
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → β
f' : α → β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
subst : ∀ {f' : α → β} (hf : ∀ (a : α), a ∈ m → f a ≍ f' a), map f m ≍ map f' m
⊢ map f m ≍ map f' m

Tactic:
subst h
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ ∀ (a : α), a ∈ m → f a = f' a

Tactic:
simp at hf
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ map f m ≍ map f' m

Tactic:
simp [map_congr rfl hf]

Premises used: Multiset.map_congr, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
p : β → Prop
s : Multiset α
⊢ (∀ (y : β), y ∈ map f s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)

Tactic:
Quotient.inductionOn' s fun _L => List.forall_mem_map

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
l : List α
⊢ map f (↑l : Multiset α) = (↑(List.map f l) : Multiset β)

Tactic:
rfl

Premises used: Multiset.map, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
⊢ map f 0 = 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
a : α
s : Multiset α
⊢ map f (a ::ₘ s) = f a ::ₘ map f s

Tactic:
Quot.inductionOn s fun _l => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
t : α
h : ∀ (x : Multiset α), (map f ∘ cons t) x = (cons (f t) ∘ map f) x
⊢ map f ∘ cons t = cons (f t) ∘ map f

Tactic:
ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
t : α
x : Multiset α
⊢ (map f ∘ cons t) x = (cons (f t) ∘ map f) x

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
a : α
⊢ map f {a} = {f a}

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.cons, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
k : ℕ
a : α
⊢ map f (replicate k a) = replicate k (f a)

Tactic:
simp only [← coe_replicate, map_coe, List.map_replicate]

Premises used: List.map_replicate, Multiset.map_coe, Multiset.coe_replicate
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
⊢ map f (s + t) = map f s + map f t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ map_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.MapFold
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
⊢ ∀ (x : α), x ∈ l → p x

Tactic:
hl

Premises used: Multiset.Mem
-- Module: Mathlib.Data.Multiset.MapFold
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
mk : ∀ (l : List β), ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (List.map c l)
⊢ ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l

Tactic:
lift l to List β using hl

Premises used: List
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst : CanLift α β c p
x : Multiset α
l : List β
⊢ ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (List.map c l)

Tactic:
⟨l, map_coe _ _⟩

Premises used: Multiset.ofList, Exists.intro, Multiset.map_coe
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst : CanLift α β c p
x : Multiset α
l : List β
⊢ ∃ (y : Multiset β), map c y = Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (List.map c l)

Tactic:
exact ⟨l, map_coe _ _⟩
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
b : β
s : Multiset α
⊢ b ∈ map f s ↔ ∃ (a : α), a ∈ s ∧ f a = b

Tactic:
Quot.inductionOn s fun _l => List.mem_map

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
⊢ (map f s).card = s.card

Tactic:
Quot.inductionOn s fun _ => length_map _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : (map f s).card = 0 ↔ s = 0
rw₁ : s.card = 0 ↔ s = 0
rw₂ rw₃ : s = 0 ↔ s = 0
⊢ map f s = 0 ↔ s = 0

Tactic:
rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]

Premises used: Multiset.card_eq_zero, Multiset.card_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : map f s = 0 ↔ s = 0
rw₁ rw₂ : s = 0 ↔ s = 0
⊢ 0 = map f s ↔ s = 0

Tactic:
rw [eq_comm, map_eq_zero]

Premises used: Multiset.map_eq_zero, eq_comm
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
a : α
s : Multiset α
h : a ∈ s
⊢ f a ∈ map f s

Tactic:
mem_map.2 ⟨_, h, rfl⟩

Premises used: Iff.mpr, Multiset.mem_map, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
mp : map f s = {b} → ∃ (a : α), s = {a} ∧ f a = b
mpr : (∃ (a : α), s = {a} ∧ f a = b) → map f s = {b}
⊢ map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.MapFold
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
rw₄ rw₅ : Eq (α := ℕ) 1 1
⊢ ∃ (a : α), s = {a}

Tactic:
rw [← card_eq_one, ← card_map, h, card_singleton]

Premises used: Multiset.card_singleton, Multiset.card_eq_one, Multiset.card_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
mp : ∀ (a : α) (ha : s = {a}), ∃ (a : α), s = {a} ∧ f a = b
⊢ ∃ (a : α), s = {a} ∧ f a = b

Tactic:
obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
-- Module: Mathlib.Data.Multiset.MapFold
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

Tactic:
⟨a, ha, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
mp : f a = b
⊢ ∃ (a : α), s = {a} ∧ f a = b

Tactic:
refine ⟨a, ha, ?_⟩
-- Module: Mathlib.Data.Multiset.MapFold
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)
mp₄ mp₅ : f a = f a
⊢ f a = b

Tactic:
rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]

Premises used: Multiset.map_singleton, Multiset.mem_singleton
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
a : α
⊢ map f {a} = {f a}

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
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
mpr : map f s = b ::ₘ t → ∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
⊢ (∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.MapFold
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)
mp₁ mp₂ : map f s = map f s
⊢ map f s = f a ::ₘ map f (s.erase a)

Tactic:
rw [← map_cons, Multiset.cons_erase ha]

Premises used: Multiset.map_cons, Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
rw : b ∈ b ::ₘ t
⊢ b ∈ map f s

Tactic:
rw [h]
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t

Tactic:
mem_cons_self _ _

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t

Tactic:
exact mem_cons_self _ _

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s

Tactic:
have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
-- Module: Mathlib.Data.Multiset.MapFold
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
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
⊢ ∃ (a : α), a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
obtain ⟨a, h1, rfl⟩ := mem_map.mp this

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.MapFold
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
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
⊢ ∃ (a_1 : α), a_1 ∈ s ∧ f a_1 = f a ∧ map f (s.erase a_1) = t

Tactic:
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Data.Multiset.MapFold
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)
⊢ map f u = t

Tactic:
rw [map_cons, cons_inj_right] at h

Premises used: Multiset.map_cons, Multiset.cons_inj_right
-- Module: Mathlib.Data.Multiset.MapFold
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)
h₁ : map f u = t
⊢ f a ∈ map f (a ::ₘ u)

Tactic:
rw [map_cons, cons_inj_right] at h

Premises used: Multiset.map_cons, Multiset.cons_inj_right
-- Module: Mathlib.Data.Multiset.MapFold
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

Tactic:
⟨a, mem_cons_self _ _, rfl, ?_⟩

Premises used: And.intro, Exists.intro, Multiset.mem_cons_self, rfl
-- Module: Mathlib.Data.Multiset.MapFold
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 ((a ::ₘ u).erase a) = t
⊢ ∃ (a_1 : α), a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Tactic:
refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
-- Module: Mathlib.Data.Multiset.MapFold
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
mpr₁ mpr₂ : t = t
⊢ map f ((a ::ₘ u).erase a) = t

Tactic:
rw [Multiset.erase_cons_head, h]

Premises used: Multiset.erase_cons_head
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
H : Injective f
a : α
s : Multiset α
⊢ f a ∈ map f s ↔ a ∈ s

Tactic:
Quot.inductionOn s fun _l => List.mem_map_of_injective H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
g : β → γ
f : α → β
s : Multiset α
⊢ map g (map f s) = map (g ∘ f) s

Tactic:
Quot.inductionOn s fun _l => congr_arg _ List.map_map

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
s : Multiset α
⊢ map id s = s

Tactic:
Quot.inductionOn s fun _l => congr_arg _ <| List.map_id _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
s : Multiset α
⊢ map (fun (x : α) ↦ x) s = s

Tactic:
map_id s

Premises used: Multiset.map_id
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
b : β
⊢ map (const α b) s = replicate s.card b

Tactic:
Quot.inductionOn s fun _ => congr_arg _ List.map_const'

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
b : β
⊢ map (fun (x : α) ↦ b) s = replicate s.card b

Tactic:
map_const _ _

Premises used: Multiset.map_const
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) (↑l : Multiset α)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : b₁ ∈ replicate (↑l : Multiset α).card b₂), b₁ ∈ replicate (↑l : Multiset α).card b₂
⊢ b₁ ∈ replicate (↑l : Multiset α).card b₂

Tactic:
rwa [map_const] at h

Premises used: Multiset.map_const
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s ≤ t
⊢ map f s ≤ map f t

Tactic:
leInductionOn h fun h => (h.map f).subperm

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t

Tactic:
(map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_

Premises used: LE.le.lt_of_not_ge, LT.lt.le, Multiset.map_le_map, Multiset.eq_of_le_of_card_le, LT.lt.ne
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
refine : ∀ (H : map f t ≤ map f s), t.card ≤ s.card
⊢ map f s < map f t

Tactic:
refine (map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_

Premises used: LE.le.lt_of_not_ge, LT.lt.le, Multiset.map_le_map, Multiset.eq_of_le_of_card_le, LT.lt.ne
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
rw : (map f t).card ≤ (map f s).card
⊢ t.card ≤ s.card

Tactic:
rw [← s.card_map f, ← t.card_map f]

Premises used: Multiset.card_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card

Tactic:
card_le_card H

Premises used: Multiset.card_le_card
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card

Tactic:
exact card_le_card H

Premises used: Multiset.card_le_card
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
⊢ Monotone (map f)

Tactic:
fun _ _ => map_le_map

Premises used: Monotone, Multiset.map_le_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
⊢ StrictMono (map f)

Tactic:
fun _ _ => map_lt_map

Premises used: StrictMono, Multiset.map_lt_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
H : s ⊆ t
⊢ map f s ⊆ map f t

Tactic:
fun _b m =>
  let ⟨a, h, e⟩ := mem_map.1 m
  mem_map.2 ⟨a, H h, e⟩

Premises used: Iff.mpr, Multiset.map, Multiset.mem_map, Membership.mem, _private.0.Multiset.map_subset_map.match_1, And.intro, Exists.intro, Iff.mp, Multiset.Subset
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
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)

Tactic:
?_
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
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)
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_

Premises used: Multiset.cons