-- 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.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
y : α
hy : l y ≠ 0
xy : y ≠ x
⊢ (single (f y) (l y)) (f x) = 0

Tactic:
simp only [SetLike.mem_coe, mem_supported, subset_def, Finset.mem_coe, mem_support_iff] at h₁

Result:
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

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
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
⊢ 0 (f x) = 0

Tactic:
rfl

Result:
no goals

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 x = 0
⊢ l x = 0 x

Tactic:
simpa

Result:
no goals

Proof state:
case neg
α : 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:
by_contra h

Result:
case neg
α : 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
h : ¬l x = 0 x
⊢ False

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 ∈ ↑(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

Tactic:
intro y hy xy

Result:
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
y : α
hy : l y ≠ 0
xy : y ≠ x
⊢ (single (f y) (l y)) (f x) = 0

Proof state:
case neg
α : 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
h : ¬l x = 0 x
⊢ False

Tactic:
exact xs (h₁ <| Finsupp.mem_support_iff.2 h)

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 : α
this : DecidablePred fun x => x ∈ s
⊢ l x = 0 x

Tactic:
by_cases xs : x ∈ s

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
⊢ l x = 0 x

case neg
α : 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

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 ∈ ↑(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

Tactic:
simp +contextual

Result:
no goals

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
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.sum fun a => single (f a)) (f x) = 0

Tactic:
rw [h₂]

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
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
⊢ 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 ∈ ↑(ker (lmapDomain M R f))
⊢ l ∈ ⊥

Tactic:
rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂

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 ∈ ⊥

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
⊢ supported M R s ⊓ ker (lmapDomain M R f) ≤ ⊥

Tactic:
rintro l ⟨h₁, h₂⟩

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 ∈ ↑(ker (lmapDomain M R f))
⊢ l ∈ ⊥