-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)}
    {toInsert : List α } (h : Perm l1 l2) (distinct : DistinctKeys l1) :
    Perm (insertListIfNewUnit l1 toInsert) (insertListIfNewUnit l2 toInsert)

Proof state:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
⊢ (if containsKey hd l1 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Tactic:
rw [contains_eq]

Result:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Proof state:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (if containsKey hd l1 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Tactic:
have contains_eq : containsKey hd l1 = containsKey hd l2 := containsKey_of_perm h

Result:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
⊢ (if containsKey hd l1 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Proof state:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Tactic:
by_cases contains_hd: containsKey hd l2 = true

Result:
case pos
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : containsKey hd l2 = true
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

case neg
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : ¬containsKey hd l2 = true
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Proof state:
case pos
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : containsKey hd l2 = true
⊢ l1.Perm l2

Tactic:
exact h

Result:
no goals

Proof state:
case neg
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : ¬containsKey hd l2 = true
⊢ l1.Perm l2

Tactic:
exact h

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertListIfNewUnit l1 (hd :: tl)).Perm (insertListIfNewUnit l2 (hd :: tl))

Tactic:
simp only [insertListIfNewUnit]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertListIfNewUnit (insertEntryIfNew hd () l1) tl).Perm (insertListIfNewUnit (insertEntryIfNew hd () l2) tl)

Proof state:
case pos
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : containsKey hd l2 = true
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Tactic:
simp only [contains_hd, ↓reduceIte]

Result:
case pos
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : containsKey hd l2 = true
⊢ l1.Perm l2

Proof state:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertEntryIfNew hd () l1).Perm (insertEntryIfNew hd () l2)

Tactic:
simp only [insertEntryIfNew, cond_eq_if]

Result:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (if containsKey hd l1 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertListIfNewUnit l1 []).Perm (insertListIfNewUnit l2 [])

Tactic:
simp [insertListIfNewUnit, h]

Result:
no goals