-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α}
    (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) :
    Disjoint (supported M R s) (ker (lmapDomain M R f))

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ l x = 0 x

Tactic:
have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
  rw [h₂]
  rfl

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : (l.sum fun a => single (f a)) (f x) = 0
⊢ l x = 0 x

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
⊢ l ∈ ⊥

Tactic:
simp only [mem_bot]

Result:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
⊢ l = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ Disjoint (supported M R s) (ker (lmapDomain M R f))

Tactic:
rw [disjoint_iff_inf_le]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ supported M R s ⊓ ker (lmapDomain M R f) ≤ ⊥

Proof state:
case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b => (single (f a₁) b) (f x)) = 0
y : α
hy : l y ≠ 0
xy : y ≠ x
h₁ : ∀ (x : α), l x ≠ 0 → x ∈ s
⊢ (single (f y) (l y)) (f x) = 0

Tactic:
simp [mt (H _ (h₁ _ hy) _ xs) xy]

Result:
no goals

Proof state:
case intro.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
⊢ l x = 0 x

Tactic:
haveI := Classical.decPred fun x => x ∈ s

Result:
case intro.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
⊢ l x = 0 x

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : (l.sum fun a => single (f a)) (f x) = 0
⊢ l x = 0 x

Tactic:
rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : l x = 0
⊢ l x = 0 x

case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b => (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b => (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
⊢ l = 0

Tactic:
ext x

Result:
case intro.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a => single (f a)) = 0
x : α
⊢ l x = 0 x