case inl
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ comapDomain f (single (f a) m) hif = single a m
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
⊢ comapDomain f (single (f a) m) hif = single a m
rcases eq_or_ne m 0 with (rfl | hm)
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0
simp only [single_zero, comapDomain_zero]
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ comapDomain f (single (f a) m) hif = single a m
rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
  support_single_ne_zero _ hm, coe_singleton, coe_singleton, single_eq_same]
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
rw [support_single_ne_zero _ hm, coe_singleton] at hif
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.304875
ι : Type ?u.304878
M : Type u_3
M' : Type ?u.304884
N : Type ?u.304887
P : Type ?u.304890
G : Type ?u.304893
H : Type ?u.304896
R : Type ?u.304899
S : Type ?u.304902
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
exact ⟨fun x hx => hif hx rfl hx, rfl⟩