Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ f = 0 ∨ (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
rw [or_iff_not_imp_left]
State after:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ ¬f = 0 → (f = fun x => 1 - x) ∨ f = fun x => x - 1

State before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ ¬f = 0 → (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
intros h1
State after:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = fun x => x - 1

State before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
apply (good_map_zero h0 h1).imp <;> intro h1
State after:
case f
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x

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

State before:
case f
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x
Tactic:
exact good_eq_of_inj h0 h1 (h f h0 h1)
State after:
no goals

State before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = -1
⊢ f = fun x => x - 1
Tactic:
rw [← neg_eq_iff_eq_neg] at h1
State after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ f = fun x => x - 1

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

State before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ f = fun x => x - 1
Tactic:
have h3 := good_eq_of_inj h2 h1 (h (-f) h2 h1)
State after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ f = fun x => x - 1

State before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ f = fun x => x - 1
Tactic:
rw [← neg_inj, h3]
State after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ (fun x => 1 - x) = -fun x => x - 1

State before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ (fun x => 1 - x) = -fun x => x - 1
Tactic:
exact funext λ x ↦ (neg_sub x 1).symm
State after:
no goals

State before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = fun x => x - 1
⊢ good f
Tactic:
rcases h0 with rfl | rfl | rfl
State after:
case inl
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good 0

case inr.inl
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good fun x => 1 - x

case inr.inr
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good fun x => x - 1

State before:
case inl
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good 0

case inr.inl
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good fun x => 1 - x

case inr.inr
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good fun x => x - 1
Tactic:
exacts [zero_is_good, one_sub_is_good, sub_one_is_good]
State after:
no goals