-- Mathlib/Data/Multiset/Pi.lean
theorem cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a}
    (h : a ≠ a') : HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f))
      (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f)) (cons (a ::ₘ m) a' b' (cons m a b f))

Tactic:
apply hfunext rfl

Result:
α : 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_1 a'_1 : α),
    HEq a_1 a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)

Proof state:
case inl
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
⊢ HEq (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₂)

Result:
case inl.inl
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)

case inl.inr
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

Proof state:
case inr
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (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]

Result:
no goals

Proof state:
α : 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_1 a'_1 : α),
    a_1 = a'_1 → HEq (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:
rintro a'' _ rfl

Result:
α : 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'' : α
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'') (cons (a ::ₘ m) a' b' (cons m a b f) a'')

Proof state:
case inl.inl
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)

case inl.inr
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (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:
all_goals simp [*, Pi.cons_same, Pi.cons_ne]

Result:
no goals

Proof state:
α : 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'' : α
⊢ HEq (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₂ _ => ?_

Result:
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

Proof state:
case inl
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (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₂)

Result:
case inl.inl
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)

case inl.inr
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)

Proof state:
α : 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_1 a'_1 : α),
    HEq a_1 a'_1 → HEq (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]

Result:
α : 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_1 a'_1 : α),
    a_1 = a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)

Proof state:
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (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)

Result:
case inl
α : 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
x✝ : HEq ha₁ ha₂
h₁ : a'' ≠ a
⊢ HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)

case inr
α : 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
x✝ : HEq ha₁ ha₂
⊢ HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)