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

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
⊢ Injective f
Tactic:
have h2 := good_shift h0 h1
State after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
⊢ Injective f

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
⊢ Injective f
Tactic:
have h3 : ∀ c d : F, d ≠ 0 → f (c + 1) = f (d + 1) →
    f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1) := λ c d h3 h4 ↦ by
  rw [good_shift2 h0 h1, ← h0, h4, add_assoc, ← add_assoc (c + 1), h2,
    good_special_equality h0 (mul_inv_cancel h3), zero_add, add_right_comm]
State after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
⊢ Injective f

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
⊢ Injective f
Tactic:
intros a b h4
State after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f a = f b
⊢ a = b

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f a = f b
⊢ a = b
Tactic:
rw [← h2 a, ← h2 b, add_left_inj] at h4
State after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
⊢ a = b

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
⊢ a = b
Tactic:
have h5 := good_map_add_one_eq_zero_iff h0 h1
State after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
⊢ a = b

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
⊢ a = b
Tactic:
rcases eq_or_ne a 0 with rfl | ha
State after:
case inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
b : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
h4 : f (0 + 1) = f (b + 1)
⊢ 0 = b

case inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
⊢ a = b

State before:
case inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
⊢ a = b
Tactic:
rcases eq_or_ne b 0 with rfl | hb
State after:
case inr.inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
h4 : f (a + 1) = f (0 + 1)
⊢ a = 0

case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b
Tactic:
have h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
  (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹))
    + a * a⁻¹ * (b * b⁻¹) := by ring
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
⊢ a = b
Tactic:
have h7 : ∀ c d : F, (c + 1) * (d + 1) = c * d + c + d + 1 := λ c d ↦ by
  rw [add_one_mul (α := F), mul_add_one (α := F), ← add_assoc]
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Tactic:
rw [mul_inv_cancel ha, mul_inv_cancel hb, mul_one, mul_one, mul_one,
  add_comm b b⁻¹, add_add_add_comm, add_comm a⁻¹ b, ← add_assoc, ← h7] at h6
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) = (a + b⁻¹ + 1) * (b + a⁻¹ + 1)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) = (a + b⁻¹ + 1) * (b + a⁻¹ + 1)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Tactic:
replace h6 := congr_arg f h6
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1)) = f ((a + b⁻¹ + 1) * (b + a⁻¹ + 1))
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1)) = f ((a + b⁻¹ + 1) * (b + a⁻¹ + 1))
⊢ a = b
Tactic:
rw [← h0, h3 a b hb h4, h3 b a ha h4.symm, h7, add_sub_cancel_right,
  h7, add_sub_cancel_right, ← h0 (a + b⁻¹ + 1), add_right_inj] at h6
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ a = b
Tactic:
replace h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) =
  a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1) := by ring
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
⊢ a = b
Tactic:
rw [mul_inv_cancel ha, mul_inv_cancel hb, one_add_one_eq_two, h, zero_add] at h7
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Tactic:
rw [← h2, ← h7, add_add_add_comm, add_add_add_comm a, ← add_add_add_comm,
  ← h0, add_right_comm, add_left_eq_self, ← h2, add_assoc,
  one_add_one_eq_two, h, add_zero, h5, mul_eq_zero, h5, h5] at h6
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Tactic:
replace h3 : ∀ c : F, -c = c := λ c ↦ by
  rw [neg_eq_iff_add_eq_zero, ← two_mul, h, zero_mul]
State after:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
⊢ a = b

State before:
case inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
⊢ a = b
Tactic:
rcases h6 with h6 | h6
State after:
case inr.inr.inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : a + b = 0
⊢ a = b

case inr.inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : b⁻¹ + a⁻¹ = 0
⊢ a = b

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
c d : F
h3 : d ≠ 0
h4 : f (c + 1) = f (d + 1)
⊢ f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
Tactic:
rw [good_shift2 h0 h1, ← h0, h4, add_assoc, ← add_assoc (c + 1), h2,
  good_special_equality h0 (mul_inv_cancel h3), zero_add, add_right_comm]
State after:
no goals

State before:
case inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
b : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
h4 : f (0 + 1) = f (b + 1)
⊢ 0 = b
Tactic:
rwa [zero_add, good_map_one h0, eq_comm, h5, eq_comm] at h4
State after:
no goals

State before:
case inr.inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
h4 : f (a + 1) = f (0 + 1)
⊢ a = 0
Tactic:
rwa [zero_add, good_map_one h0, h5] at h4
State after:
no goals

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
Tactic:
ring
State after:
no goals

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
c d : F
⊢ (c + 1) * (d + 1) = c * d + c + d + 1
Tactic:
rw [add_one_mul (α := F), mul_add_one (α := F), ← add_assoc]
State after:
no goals

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
Tactic:
ring
State after:
no goals

State before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
c : F
⊢ -c = c
Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul, h, zero_mul]
State after:
no goals

State before:
case inr.inr.inl
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : a + b = 0
⊢ a = b
Tactic:
rwa [add_eq_zero_iff_eq_neg, h3] at h6
State after:
no goals

State before:
case inr.inr.inr
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : b⁻¹ + a⁻¹ = 0
⊢ a = b
Tactic:
rwa [add_eq_zero_iff_eq_neg, h3, inv_inj, eq_comm] at h6
State after:
no goals