awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
rw :
  LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
rw₁ rw₂ :
  LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m < 1

Tactic:
rw [← (toNNReal_strictMono he).lt_iff_lt, map_one]

Premises used: StrictMono.lt_iff_lt, map_one, WithZeroMulInt.toNNReal_strictMono
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
rw :
  LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 1 : ℝ≥0)
rw₁ rw₂ :
  LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔
    LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m ≤ 1

Tactic:
rw [← (toNNReal_strictMono he).le_iff_le, map_one]

Premises used: map_one, WithZeroMulInt.toNNReal_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : l₁.NodupKeys (β := β)
l₂ : List (Sigma β)
nodupKeys : l₂.NodupKeys (β := β)
H : (mk (β := β) l₁ h₁).entries (β := β) = (mk (β := β) l₂ nodupKeys).entries (β := β)
⊢ mk (β := β) l₁ h₁ = mk (β := β) l₂ nodupKeys

Tactic:
congr
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
xs ys : AList β
rw : Decidable (xs.entries (β := β) = ys.entries (β := β))
⊢ Decidable (xs = ys)

Tactic:
rw [AList.ext_iff]

Premises used: AList.ext_iff
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries (β := β) = ys.entries (β := β))

Tactic:
infer_instance
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s : AList β
⊢ s.keys (β := β).Nodup

Tactic:
s.nodupKeys

Premises used: AList.keys, List.NodupKeys, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (mk (β := β) l h).keys (β := β) = l.keys (β := β)

Tactic:
rfl

Premises used: AList.keys, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
a : α
s : AList β
⊢ a ∈ s ↔ a ∈ s.keys (β := β)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
a : α
s₁ s₂ : AList β
p : s₁.entries (β := β) ~ s₂.entries (β := β)
⊢ a ∈ s₁ ↔ a ∈ s₂

Tactic:
(p.map Sigma.fst).mem_iff

Premises used: List.keys, Sigma.fst, AList.keys, List.Perm.map, List.Perm.mem_iff
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
h : l.NodupKeys (β := β)
x : α
⊢ x ∈ mk (β := β) l h ↔ x ∈ l.keys (β := β)

Tactic:
.rfl

Premises used: Iff.rfl, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
a : α
⊢ ¬Membership.mem (γ := AList β) ∅ a

Tactic:
not_mem_nil

Premises used: List.map, List.keys, AList.keys, List.not_mem_nil
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
⊢ Eq (α := List (Sigma β)) (entries (β := β) ∅) []

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
⊢ Eq.{u + 1} (α := List α) (keys (β := β) ∅) []

Tactic:
rfl

Premises used: List.map, List.keys, AList.keys, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
a : α
b : β a
⊢ (singleton (β := β) a b).entries (β := β) = [Sigma.mk (β := β) a b]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
a : α
b : β a
⊢ (singleton (β := β) a b).keys (β := β) = [a]

Tactic:
rfl

Premises used: List.map, List.keys, AList.keys, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := Option (β a)) (lookup (β := β) a ∅) none

Tactic:
rfl

Premises used: AList.lookup, List.dlookup, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ (lookup (β := β) a s).isSome = true ↔ a ∈ s

Tactic:
dlookup_isSome

Premises used: AList.lookup, List.dlookup_isSome, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ lookup (β := β) a s = none ↔ ¬a ∈ s

Tactic:
dlookup_eq_none

Premises used: List.dlookup_eq_none, AList.lookup, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ b ∈ lookup (β := β) a s ↔ Sigma.mk (β := β) a b ∈ s.entries (β := β)

Tactic:
mem_dlookup_iff s.nodupKeys

Premises used: AList.lookup, List.mem_dlookup_iff, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
p : s₁.entries (β := β) ~ s₂.entries (β := β)
⊢ lookup (β := β) a s₁ = lookup (β := β) a s₂

Tactic:
perm_dlookup _ s₁.nodupKeys p

Premises used: List.perm_dlookup, AList.lookup, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this : DecidableEq α := Classical.decEq α
⊢ Sigma.mk (β := β) k ((lookup (β := β) k s₁).get ⋯) ∈ s₂.entries (β := β)

Tactic:
have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : Sigma.mk (β := β) k ((lookup (β := β) k s₁).get ⋯) ∈ s₂.entries (β := β)
⊢ lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get ⋯)

Tactic:
rw [← mem_lookup_iff, Option.mem_def] at this

Premises used: AList.mem_lookup_iff, Option.mem_def
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get ⋯)
rw : (some ((lookup (β := β) k s₁).get ⋯)).isSome = true
⊢ k ∈ s₂.keys (β := β)

Tactic:
rw [← mem_keys, ← lookup_isSome, this]

Premises used: AList.mem_keys, AList.lookup_isSome
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get ⋯)
⊢ (some ((lookup (β := β) k s₁).get ⋯)).isSome = true

Tactic:
Option.isSome_some

Premises used: Option.isSome_some
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries (β := β) ⊆ s₂.entries (β := β)
k : α
hk : k ∈ s₁.keys (β := β)
this_1 : DecidableEq α := Classical.decEq α
this : lookup (β := β) k s₂ = some ((lookup (β := β) k s₁).get ⋯)
⊢ (some ((lookup (β := β) k s₁).get ⋯)).isSome = true

Tactic:
exact Option.isSome_some

Premises used: Option.isSome_some
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ (replace (β := β) a b s).keys (β := β) = s.keys (β := β)

Tactic:
keys_kreplace _ _ _

Premises used: List.kreplace, List.keys_kreplace, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s : AList β
rw : a' ∈ (replace (β := β) a b s).keys (β := β) ↔ a' ∈ s
rw₁ : a' ∈ s.keys (β := β) ↔ a' ∈ s
rw₂ rw₃ : a' ∈ s ↔ a' ∈ s
⊢ a' ∈ replace (β := β) a b s ↔ a' ∈ s

Tactic:
rw [mem_keys, keys_replace, ← mem_keys]

Premises used: AList.mem_keys, AList.keys_replace
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ s₁.entries (β := β) ~ s₂.entries (β := β) →
    (replace (β := β) a b s₁).entries (β := β) ~ (replace (β := β) a b s₂).entries (β := β)

Tactic:
Perm.kreplace s₁.nodupKeys

Premises used: List.kreplace, AList.nodupKeys, List.Perm.kreplace
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ (erase (β := β) a s).keys (β := β) = s.keys (β := β).erase a

Tactic:
keys_kerase

Premises used: List.kerase, List.keys_kerase, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
rw : a' ∈ (erase (β := β) a s).keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
rw₁ : a' ∈ s.keys (β := β).erase a ↔ a' ≠ a ∧ a' ∈ s
rw₂ : a' ≠ a ∧ a' ∈ s.keys (β := β) ↔ a' ≠ a ∧ a' ∈ s
rw₃ rw₄ : a' ≠ a ∧ a' ∈ s ↔ a' ≠ a ∧ a' ∈ s
⊢ a' ∈ erase (β := β) a s ↔ a' ≠ a ∧ a' ∈ s

Tactic:
rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]

Premises used: AList.keys_nodup, AList.mem_keys, AList.keys_erase, List.Nodup.mem_erase_iff
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
⊢ s₁.entries (β := β) ~ s₂.entries (β := β) →
    (erase (β := β) a s₁).entries (β := β) ~ (erase (β := β) a s₂).entries (β := β)

Tactic:
Perm.kerase s₁.nodupKeys

Premises used: List.Perm.kerase, List.kerase, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ lookup (β := β) a (erase (β := β) a s) = none

Tactic:
dlookup_kerase a s.nodupKeys

Premises used: List.dlookup_kerase, List.kerase, AList.lookup, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
h : a ≠ a'
⊢ lookup (β := β) a (erase (β := β) a' s) = lookup (β := β) a s

Tactic:
dlookup_kerase_ne h

Premises used: List.dlookup_kerase_ne, List.kerase, AList.lookup
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s : AList β
⊢ erase (β := β) a' (erase (β := β) a s) = erase (β := β) a (erase (β := β) a' s)

Tactic:
ext <| kerase_kerase

Premises used: AList.ext, List.kerase_kerase
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ (insert (β := β) a b s).entries (β := β) = Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))

Tactic:
rfl

Premises used: List.kinsert, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
rw : Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β)) = Sigma.mk (β := β) a b :: s.entries (β := β)
rw₁ rw₂ : Sigma.mk (β := β) a b :: s.entries (β := β) = Sigma.mk (β := β) a b :: s.entries (β := β)
⊢ (insert (β := β) a b s).entries (β := β) = Sigma.mk (β := β) a b :: s.entries (β := β)

Tactic:
rw [entries_insert, kerase_of_notMem_keys h]

Premises used: List.kerase_of_notMem_keys, AList.entries_insert
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ insert (β := β) a b s = mk (β := β) (Sigma.mk (β := β) a b :: s.entries (β := β)) ⋯

Tactic:
ext <| entries_insert_of_notMem h

Premises used: AList.ext, AList.entries_insert_of_notMem
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
⊢ insert (β := β) a b ∅ = singleton (β := β) a b

Tactic:
rfl

Premises used: AList.insert, List.kerase, AList.singleton, List.kinsert, List.eraseP, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
s : AList β
⊢ a ∈ insert (β := β) a' b' s ↔ a = a' ∨ a ∈ s

Tactic:
mem_keys_kinsert

Premises used: AList.keys, List.kinsert, List.mem_keys_kinsert
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ (insert (β := β) a b s).keys (β := β) = a :: s.keys (β := β).erase a

Tactic:
simp [insert, keys, keys_kerase]

Premises used: AList.insert, List.keys_kerase, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries (β := β) ~ s₂.entries (β := β)
⊢ Sigma.mk (β := β) a b :: kerase (β := β) a (s₁.entries (β := β)) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (s₂.entries (β := β))

Tactic:
p.kinsert s₁.nodupKeys

Premises used: List.Perm.kinsert, List.kinsert, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries (β := β) ~ s₂.entries (β := β)
⊢ Sigma.mk (β := β) a b :: kerase (β := β) a (s₁.entries (β := β)) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (s₂.entries (β := β))

Tactic:
exact p.kinsert s₁.nodupKeys

Premises used: List.Perm.kinsert, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ lookup (β := β) a (insert (β := β) a b s) = some b

Tactic:
simp only [lookup, insert, dlookup_kinsert]

Premises used: AList.insert, AList.lookup, List.dlookup_kinsert
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
s : AList β
h : a ≠ a'
⊢ lookup (β := β) a (insert (β := β) a' b' s) = lookup (β := β) a s

Tactic:
dlookup_kinsert_ne h

Premises used: AList.lookup, List.kinsert, List.dlookup_kinsert_ne
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
pos : ∀ (h : k' = k), lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
neg : ∀ (h : ¬k' = k), lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none

Tactic:
by_cases h : k' = k
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
h : k' = k
pos : ∀ {v : β k'}, lookup (β := β) k' (insert (β := β) k' v l) = none ↔ k' ≠ k' ∧ lookup (β := β) k' l = none
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none

Tactic:
subst h
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup (β := β) k' (insert (β := β) k' v l) = none ↔ k' ≠ k' ∧ lookup (β := β) k' l = none

Tactic:
simp
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
k k' : α
v : β k
h : ¬k' = k
⊢ lookup (β := β) k' (insert (β := β) k v l) = none ↔ k' ≠ k ∧ lookup (β := β) k' l = none

Tactic:
simp_all [lookup_insert_ne h]

Premises used: AList.lookup_insert_ne
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (mk (β := β) (s.dedupKeys (β := β)) ⋯) = dlookup (β := β) a s
rw₁ : dlookup (β := β) a ((mk (β := β) (s.dedupKeys (β := β)) ⋯).entries (β := β)) = dlookup (β := β) a s
rw₂ rw₃ : dlookup (β := β) a s = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s

Tactic:
rw [List.toAList, lookup, dlookup_dedupKeys]

Premises used: List.dlookup_dedupKeys, AList.lookup, List.toAList
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
s : AList β
a₁ : (insert (β := β) a b' (insert (β := β) a b s)).entries (β := β) = (insert (β := β) a b' s).entries (β := β)
⊢ insert (β := β) a b' (insert (β := β) a b s) = insert (β := β) a b' s

Tactic:
ext : 1
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert (β := β) a b' (insert (β := β) a b s)).entries (β := β) = (insert (β := β) a b' s).entries (β := β)

Tactic:
simp only [AList.entries_insert, List.kerase_cons_eq]

Premises used: AList.entries_insert, List.kerase_cons_eq
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₁ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₂ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))

Tactic:
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]

Premises used: List.kerase_comm, List.kerase_cons_ne
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))

Tactic:
apply Perm.swap

Premises used: List.Perm.swap
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a ≠ (Sigma.mk (β := β) a' b').fst (β := β)

Tactic:
h
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a ≠ (Sigma.mk (β := β) a' b').fst (β := β)

Tactic:
exact h
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a' ≠ (Sigma.mk (β := β) a b).fst (β := β)

Tactic:
h.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a' ≠ (Sigma.mk (β := β) a b).fst (β := β)

Tactic:
exact h.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
rw₁ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₂ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₃ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₄ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₅ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₆ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₇ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₈ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₉ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₁₀ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₁₁ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₁₂ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₁₃ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₁₄ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₁₅ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₁₆ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))

Tactic:
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]

Premises used: List.kerase_comm, List.kerase_cons_ne, Ne.symm, List.Perm.swap
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
⊢ (insert (β := β) a b (singleton (β := β) a b')).entries (β := β) = (singleton (β := β) a b).entries (β := β)

Tactic:
simp only [AList.entries_insert, List.kerase_cons_eq, AList.singleton_entries]

Premises used: AList.entries_insert, List.kerase_cons_eq, AList.singleton_entries
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List (Sigma β)
⊢ xs.toAList (β := β).entries (β := β) = xs.dedupKeys (β := β)

Tactic:
rfl

Premises used: List.dedupKeys, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
xs : List (Sigma β)
⊢ (Sigma.mk (β := β) a b :: xs).toAList (β := β) = insert (β := β) a b (xs.toAList (β := β))

Tactic:
rfl

Premises used: AList.insert, List.toAList, List.kinsert, List.dedupKeys, List.foldr, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
⊢ mk (β := β) (c :: l) h = insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯)

Tactic:
simpa [insert] using (kerase_of_notMem_keys <| notMem_keys_of_nodupKeys_cons h).symm

Premises used: List.kerase_of_notMem_keys, AList.insert, Eq.symm, List.notMem_keys_of_nodupKeys_cons
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
rw : C (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯))
⊢ C (mk (β := β) (c :: l) h)

Tactic:
rw [mk_cons_eq_insert]

Premises used: AList.mk_cons_eq_insert
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
refine : ¬c.fst (β := β) ∈ mk (β := β) l ⋯
⊢ C (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯))

Tactic:
refine IH _ _ _ ?_ (insertRec H0 IH _)
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
⊢ ¬c.fst (β := β) ∈ mk (β := β) l ⋯

Tactic:
notMem_keys_of_nodupKeys_cons h

Premises used: AList.keys, List.notMem_keys_of_nodupKeys_cons
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
⊢ ¬c.fst (β := β) ∈ mk (β := β) l ⋯

Tactic:
exact notMem_keys_of_nodupKeys_cons h

Premises used: List.notMem_keys_of_nodupKeys_cons
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
H0 : True
IH : ∀ (a : α) (b : β a) (l : AList β), ¬a ∈ l → True → True
⊢ True

Tactic:
induction l
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
⊢ True

Tactic:
trivial