-- Mathlib/Data/Finsupp/Basic.lean
theorem extendDomain_single (a : Subtype P) (m : M) :
    (single a m).extendDomain = single a.val m

Proof state:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
h : P a'
⊢ a ≠ ⟨a', h⟩

Tactic:
simp [Subtype.ext_iff, ha]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ (if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'

Tactic:
obtain rfl | ha := eq_or_ne a.val a'

Result:
case h.inl
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (if h : P ↑a then (single a m) ⟨↑a, h⟩ else 0) = (single (↑a) m) ↑a

case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
⊢ (if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'

Proof state:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
⊢ ∀ (h : P a'), (single a m) ⟨a', h⟩ = 0

Tactic:
intro h

Result:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
h : P a'
⊢ (single a m) ⟨a', h⟩ = 0

Proof state:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
⊢ (if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'

Tactic:
simp_rw [single_eq_of_ne ha, dite_eq_right_iff]

Result:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
⊢ ∀ (h : P a'), (single a m) ⟨a', h⟩ = 0

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain = single (↑a) m

Tactic:
ext a'

Result:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ (single a m).extendDomain a' = (single (↑a) m) a'

Proof state:
case h.inl
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (if h : P ↑a then (single a m) ⟨↑a, h⟩ else 0) = (single (↑a) m) ↑a

Tactic:
simp_rw [single_eq_same, dif_pos a.prop]

Result:
no goals

Proof state:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
h : P a'
⊢ (single a m) ⟨a', h⟩ = 0

Tactic:
rw [single_eq_of_ne]

Result:
case h.inr
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : ↑a ≠ a'
h : P a'
⊢ a ≠ ⟨a', h⟩

Proof state:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ (single a m).extendDomain a' = (single (↑a) m) a'

Tactic:
rw [extendDomain_toFun]

Result:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ (if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'