Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective (Compfiles/Imo2017P2.lean)

State before:
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
Tactic:
constructor
State after:
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

State before:
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
Tactic:
rw [or_iff_not_imp_left]
State after:
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

State before:
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
Tactic:
intros h0 h1
State after:
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
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x

State before:
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
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Tactic:
apply (good_map_zero h0 h1).imp <;> intro h1
State after:
case mp.f
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
⊢ f = -fun x => 1 - x

State before:
case mp.f
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
Tactic:
exact good_eq_of_inj h0 h1 (h f h0 h1)
State after:
no goals

State before:
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
Tactic:
rw [← neg_eq_iff_eq_neg] at h1 ⊢
State after:
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

State before:
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
Tactic:
have h2 := good_neg h0
State after:
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

State before:
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
Tactic:
exact good_eq_of_inj h2 h1 (h (-f) h2 h1)
State after:
no goals

State before:
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
Tactic:
intro h0
State after:
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
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
⊢ good f

State before:
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
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
⊢ good f
Tactic:
rcases h0 with rfl | rfl | rfl
State after:
case mpr.inl
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
⊢ good 0

case mpr.inr.inl
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
⊢ good fun x => 1 - x

case mpr.inr.inr
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
⊢ good (-fun x => 1 - x)

State before:
case mpr.inl
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
⊢ good 0

case mpr.inr.inl
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
⊢ good fun x => 1 - x

case mpr.inr.inr
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
⊢ good (-fun x => 1 - x)
Tactic:
exacts [good_zero, good_one_sub, good_neg good_one_sub]
State after:
no goals