have h2 := good_neg h0
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ -f = fun x => 1 - x
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ -f = fun x => 1 - x