α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
⊢ f = g
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ Injective graph
intro f g h
no goals
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
⊢ f = g
classical
  have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
  refine' ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ _⟩
  exact mk_mem_graph _ (hsup ▸ hx)
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
hsup : f.support = g.support
⊢ f = g
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
⊢ f = g
have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ (x, ↑g x) ∈ graph g
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
hsup : f.support = g.support
⊢ f = g
refine' ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ _⟩
no goals
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ (x, ↑g x) ∈ graph g
exact mk_mem_graph _ (hsup ▸ hx)
no goals
α✝ : Type ?u.4285
β : Type ?u.4288
γ : Type ?u.4291
ι : Type ?u.4294
M✝ : Type ?u.4297
M' : Type ?u.4300
N : Type ?u.4303
P : Type ?u.4306
G : Type ?u.4309
H : Type ?u.4312
R : Type ?u.4315
S : Type ?u.4318
inst✝¹ : Zero M✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
f g : α →₀ M
h : graph f = graph g
⊢ f.support = g.support
rw [← image_fst_graph, h, image_fst_graph]