constructor
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
⊢ good f ↔ f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
case mp
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
⊢ good f → f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x

case mpr
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
⊢ (f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x) → good f