awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) → s.Nodup → (map f s).Nodup

Tactic:
Quot.induction_on s fun _ => List.Nodup.map_on

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
hf : Injective f
⊢ s.Nodup → (Multiset.map f s).Nodup

Tactic:
Nodup.map_on fun _ _ _ _ h => hf h

Premises used: Multiset.Nodup.map_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
d : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y
⊢ (map f s).Nodup ↔ s.Nodup

Tactic:
⟨Nodup.of_map _, fun h => h.map_on d⟩

Premises used: Iff.intro, Multiset.Nodup.of_map, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
d : Injective f
⊢ (map f s).Nodup ↔ s.Nodup

Tactic:
⟨Nodup.of_map _, fun h => h.map d⟩

Premises used: Multiset.Nodup.map, Iff.intro, Multiset.Nodup.of_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
⊢ (map f s).Nodup → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y

Tactic:
Quot.induction_on s fun _ => List.inj_on_of_nodup_map

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
d : s.Nodup
⊢ (map f s).Nodup ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y

Tactic:
⟨inj_on_of_nodup_map, fun h => d.map_on h⟩

Premises used: Multiset.inj_on_of_nodup_map, Iff.intro, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
H : ∀ (a : α), a ∈ s → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
⊢ s.Nodup → (Multiset.pmap (p := p) f s H).Nodup

Tactic:
Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
s : Multiset α
⊢ s.attach.Nodup ↔ s.Nodup

Tactic:
Quot.induction_on s fun _ => List.nodup_attach

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
rw : ∀ (a : β), a ∈ t ↔ Membership.mem (γ := Multiset β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach) a
rw₁ : Nodup.{v} (α := β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach)
⊢ t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach

Tactic:
rw [ht.ext]

Premises used: Multiset.Nodup.ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ ∀ (a : β), a ∈ t ↔ Membership.mem (γ := Multiset β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach) a

Tactic:
aesop
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ Nodup.{v} (α := β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach)

Tactic:
hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy

Premises used: Multiset.Nodup.map, Multiset.Nodup.attach, Subtype.val, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ Nodup.{v} (α := β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach)

Tactic:
exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy

Premises used: Multiset.Nodup.map, Multiset.Nodup.attach, Subtype.val, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach

Tactic:
have : t = s.attach.map fun x => i x.1 x.2 := by
    rw [ht.ext]
    · aesop
    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
rw rw₁ : map f s = map f s
⊢ map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯

Tactic:
rw [pmap_eq_map]

Premises used: Multiset.pmap_eq_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
rw rw₁ :
  Eq.{u_2 + 1} (α := Multiset γ) (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
    (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
⊢ Eq.{u_2 + 1} (α := Multiset γ) (pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯)
    (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)

Tactic:
rw [pmap_eq_map_attach]

Premises used: Multiset.pmap_eq_map_attach
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
rw :
  map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach =
    map (g ∘ fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach = map g t

Tactic:
rw [this, Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach =
    map (g ∘ fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach

Tactic:
map_congr rfl fun x _ => h _ _

Premises used: Multiset.map_congr, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach =
    map (g ∘ fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach

Tactic:
exact map_congr rfl fun x _ => h _ _

Premises used: Multiset.map_congr, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
f₁ : map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯
f₂ :
  Eq.{u_2 + 1} (α := Multiset γ) (pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯)
    (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
f₃ : map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach = map g t
⊢ map f s = map g t

Tactic:
calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

Premises used: Multiset.map, id, Multiset.pmap, Multiset.attach
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
x : ℕ × ℕ
rw : x ∈ (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) ↔ x.1 + x.2 = n
rw₁ : x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
rw₂ rw₃ : x.1 + x.2 = n ↔ x.1 + x.2 = n
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n

Tactic:
rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]

Premises used: Multiset.mem_coe, Multiset.Nat.antidiagonal, List.Nat.mem_antidiagonal
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)).card = n + 1
rw₁ : (List.Nat.antidiagonal n).length = n + 1
rw₂ rw₃ : n + 1 = n + 1
⊢ (antidiagonal n).card = n + 1

Tactic:
rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]

Premises used: List.Nat.length_antidiagonal, Multiset.Nat.antidiagonal, Multiset.coe_card
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
⊢ antidiagonal 0 = {(0, 0)}

Tactic:
rfl

Premises used: List.map, Multiset.cons, Multiset.Nat.antidiagonal, Multiset.ofList, rfl, List.Nat.antidiagonal
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
⊢ (antidiagonal n).Nodup

Tactic:
coe_nodup.2 <| List.Nat.nodup_antidiagonal n

Premises used: Iff.mpr, Multiset.Nat.antidiagonal, Multiset.coe_nodup, List.Nat.nodup_antidiagonal
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
simp only [antidiagonal, List.Nat.antidiagonal_succ, map_coe, cons_coe]

Premises used: Multiset.Nat.antidiagonal, List.Nat.antidiagonal_succ, Multiset.cons_coe, Multiset.map_coe
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₄ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₅ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₆ :
  (↑([(n + 1, 0)] ++ List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₇ :
  (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₈ rw₉ :
  (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]

Premises used: Multiset.coe_add, Multiset.add_comm, Multiset.Nat.antidiagonal, List.singleton_append, Multiset.cons_coe, Multiset.map_coe, List.Nat.antidiagonal_succ'
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
rw :
  (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]

Premises used: Multiset.map_cons, Multiset.Nat.antidiagonal_succ, Multiset.Nat.antidiagonal_succ', Prod.map_apply, Multiset.map_map
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.NatAntidiagonal
Goal:
n : ℕ
rw : map Prod.swap (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₁ :
  (↑(List.map Prod.swap (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₂ : (↑(List.Nat.antidiagonal n).reverse : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₃ rw₄ : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
⊢ map Prod.swap (antidiagonal n) = antidiagonal n

Tactic:
rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]

Premises used: Multiset.Nat.antidiagonal, List.Nat.map_swap_antidiagonal, Multiset.map_coe, Multiset.coe_reverse
-- Module: Mathlib.Data.Multiset.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
s : Multiset α
H : Symmetric r
hs : Pairwise r s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≠ b → r a b

Tactic:
let ⟨_, hl₁, hl₂⟩ := hs
  hl₁.symm ▸ hl₂.forall H

Premises used: Eq.rec, _private.0.Multiset.Pairwise.forall.match_1, List.Pairwise.forall, Eq.symm
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a : α) → a ∈ m → δ a
h : a ∈ a ::ₘ m
⊢ cons (δ := δ) m a b f a h = b

Tactic:
dif_pos rfl

Premises used: dif_pos, Multiset.Pi.cons, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a a' : α
b : δ a
f : (a : α) → a ∈ m → δ a
h' : a' ∈ a ::ₘ m
h : a' ≠ a
⊢ cons (δ := δ) m a b f a' h' = f a' ⋯

Tactic:
dif_neg h

Premises used: dif_neg, Multiset.Pi.cons
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
apply :
  ∀ (a_1 a'_1 : α),
    a_1 ≍ a'_1 →
      cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
        cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) ≍ cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f)

Tactic:
apply hfunext rfl

Premises used: Function.hfunext, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
simp :
  ∀ (a_1 a'_1 : α),
    a_1 = a'_1 →
      cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
        cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1
⊢ ∀ (a_1 a'_1 : α),
    a_1 ≍ a'_1 →
      cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
        cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1

Tactic:
simp only [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
rw rw₁ : (a'' ∈ a' ::ₘ a ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)

Tactic:
rw [Multiset.cons_swap]

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
refine :
  ∀ (ha₁ : a'' ∈ a ::ₘ a' ::ₘ m) (ha₂ : a'' ∈ a' ::ₘ a ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
        cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ≍ cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a''

Tactic:
refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_

Premises used: Function.hfunext
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
inl :
  ∀ (h₁ : a'' ≠ a),
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
inr :
  ∀ {b : δ a''} (h : a'' ≠ a') (ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m) (ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a' ::ₘ m) a'' b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
        cons (δ := δ) (a'' ::ₘ m) a' b' (cons (δ := δ) m a'' b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂

Tactic:
rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)

Premises used: Decidable.ne_or_eq, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
inl :
  ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
        cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
inl₁ :
  ∀ (h₂ : a'' ≠ a'),
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂

Tactic:
rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
inl :
  ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
        cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
inl₁ :
  ∀ (h₂ : a'' ≠ a'),
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂

Tactic:
on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
⊢ cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

Premises used: Multiset.Pi.cons_same, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

Premises used: Multiset.Pi.cons_same, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
h_1 : ha₁ ≍ ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a'' b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a'' ::ₘ m) a' b' (cons (δ := δ) m a'' b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

Premises used: Multiset.Pi.cons_same, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
h : ∀ (a' : α) (h' : a' ∈ a ::ₘ m), cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
⊢ (cons (δ := δ) m a (f a ⋯) fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) = f

Tactic:
ext a' h'
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
pos : ∀ (h : a' = a), cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
neg : ∀ (h : ¬a' = a), cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'

Tactic:
by_cases h : a' = a