Theorem: Imo2009P5.final_solution_nat (Compfiles/Imo2009P5.lean)

State before:
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) ↔
    f = fun x => x
Tactic:
symm
State after:
f : ℕ → ℕ
⊢ (f = fun x => x) ↔
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x

State before:
f : ℕ → ℕ
⊢ (f = fun x => x) ↔
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
Tactic:
constructor
State after:
case mp
f : ℕ → ℕ
⊢ (f = fun x => x) →
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x

case mpr
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) →
    f = fun x => x

State before:
case mpr
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) →
    f = fun x => x
Tactic:
rintro ⟨h, h0, h1⟩
State after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f = fun x => x

State before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f = fun x => x
Tactic:
replace h1 : f 0 = 0 := by
  contrapose! h0; rw [← zero_lt_iff] at h0
  obtain ⟨K, h2⟩ := exists_sup_fn_fin f (f 0)
  refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
  rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
  exact h2 _ (Nat.mod_lt (f (K + K + 1)) h0)
State after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ f = fun x => x

State before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ f = fun x => x
Tactic:
replace h0 : ∀ x : ℕ, f (f x) = x := by
  intros x; apply le_antisymm
  replace h := h x 0
  rwa [h1, zero_add, zero_add] at h
  replace h0 := h0 x 0
  rwa [h1, zero_add, zero_add] at h0
State after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
⊢ f = fun x => x

State before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
⊢ f = fun x => x
Tactic:
replace h := h 1
State after:
case mpr.intro.intro
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ f = fun x => x

State before:
case mpr.intro.intro
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
⊢ f = fun x => x
Tactic:
funext x
State after:
case mpr.intro.intro.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
⊢ f x = x

State before:
case mpr.intro.intro.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
⊢ f x = x
Tactic:
induction' x using Nat.strong_induction_on with x x_ih
State after:
case mpr.intro.intro.h.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x, f m = m
⊢ f x = x

State before:
case mpr.intro.intro.h.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x, f m = m
⊢ f x = x
Tactic:
cases' x with x
State after:
case mpr.intro.intro.h.h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x_ih : ∀ m < 0, f m = m
⊢ f 0 = 0

case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1
Tactic:
replace h := h x
State after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + f 1) ≤ f x + 1
⊢ f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + f 1) ≤ f x + 1
⊢ f (x + 1) = x + 1
Tactic:
rw [h2, x_ih x x.lt_succ_self, le_iff_eq_or_lt, Nat.lt_succ_iff] at h
State after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) = x + 1 ∨ f (x + 1) ≤ x
⊢ f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) = x + 1 ∨ f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Tactic:
revert h
State after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1 ∨ f (x + 1) ≤ x → f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1 ∨ f (x + 1) ≤ x → f (x + 1) = x + 1
Tactic:
refine (or_iff_left_of_imp (λ h ↦ ?_)).mp
State after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) ≤ x
⊢ f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Tactic:
replace x_ih := congr_arg f (x_ih _ (lt_of_le_of_lt h x.lt_succ_self))
State after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
h : f (x + 1) ≤ x
x_ih : f (f (f (x + 1))) = f (f (x + 1))
⊢ f (x + 1) = x + 1

State before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
h : f (x + 1) ≤ x
x_ih : f (f (f (x + 1))) = f (f (x + 1))
⊢ f (x + 1) = x + 1
Tactic:
rwa [h0, h0] at x_ih
State after:
no goals

State before:
case mp
f : ℕ → ℕ
⊢ (f = fun x => x) →
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
Tactic:
rintro rfl
State after:
case mp

⊢ (∀ (x y : ℕ), (fun x => x) (y + (fun x => x) x) ≤ (fun x => x) y + x) ∧
    (∀ (x y : ℕ), x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)) ∧
      ∀ (x y : ℕ), (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x

State before:
case mp

⊢ (∀ (x y : ℕ), (fun x => x) (y + (fun x => x) x) ≤ (fun x => x) y + x) ∧
    (∀ (x y : ℕ), x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)) ∧
      ∀ (x y : ℕ), (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Tactic:
refine ⟨λ x y ↦ le_refl (y + x), λ x y ↦ ?_, λ x y ↦ ?_⟩
State after:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)

case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x

State before:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Tactic:
rw [add_assoc]
State after:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ y + ((fun x => x) x + x)

State before:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ y + ((fun x => x) x + x)
Tactic:
exact le_self_add
State after:
no goals

State before:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)
Tactic:
rw [← add_assoc]
State after:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + y + (fun x => x) x

State before:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + y + (fun x => x) x
Tactic:
exact le_add_self
State after:
no goals

State before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f 0 = 0
Tactic:
contrapose! h0
State after:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : f 0 ≠ 0
⊢ ∃ x y, f y + f (y + f x) < x

State before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : f 0 ≠ 0
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
rw [← zero_lt_iff] at h0
State after:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
⊢ ∃ x y, f y + f (y + f x) < x

State before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
obtain ⟨K, h2⟩ := exists_sup_fn_fin f (f 0)
State after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ ∃ x y, f y + f (y + f x) < x

State before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
State after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (0 + f (K + K + 1)) ≤ K

State before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (0 + f (K + K + 1)) ≤ K
Tactic:
rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
State after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (f (K + K + 1) % f 0) ≤ K

State before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (f (K + K + 1) % f 0) ≤ K
Tactic:
exact h2 _ (Nat.mod_lt (f (K + K + 1)) h0)
State after:
no goals

State before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ ∀ (x : ℕ), f (f x) = x
Tactic:
intros x
State after:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ f (f x) = x

State before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ f (f x) = x
Tactic:
apply le_antisymm
State after:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ f (f x) ≤ x

case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)

State before:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ f (f x) ≤ x

case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)
Tactic:
replace h := h x 0
State after:
case a
f : ℕ → ℕ
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
h : f (0 + f x) ≤ f 0 + x
⊢ f (f x) ≤ x

case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)

State before:
case a
f : ℕ → ℕ
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
h : f (0 + f x) ≤ f 0 + x
⊢ f (f x) ≤ x

case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)
Tactic:
rwa [h1, zero_add, zero_add] at h
State after:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)

State before:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
⊢ x ≤ f (f x)
Tactic:
replace h0 := h0 x 0
State after:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
x : ℕ
h0 : x ≤ f 0 + f (0 + f x)
⊢ x ≤ f (f x)

State before:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
x : ℕ
h0 : x ≤ f 0 + f (0 + f x)
⊢ x ≤ f (f x)
Tactic:
rwa [h1, zero_add, zero_add] at h0
State after:
no goals

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ f 1 = 1
Tactic:
suffices this : ∀ n : ℕ, f (n * f 1) = n by
  replace this := congr_arg f (this (f 1))
  rw [h0, h0] at this
  exact Nat.eq_one_of_mul_eq_one_left this
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ ∀ (n : ℕ), f (n * f 1) = n

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ ∀ (n : ℕ), f (n * f 1) = n
Tactic:
intro n
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
⊢ f (n * f 1) = n

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
⊢ f (n * f 1) = n
Tactic:
induction' n using Nat.strong_induction_on with n n_ih
State after:
case h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n, f (m * f 1) = m
⊢ f (n * f 1) = n

State before:
case h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n, f (m * f 1) = m
⊢ f (n * f 1) = n
Tactic:
cases' n with n
State after:
case h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n_ih : ∀ m < 0, f (m * f 1) = m
⊢ f (0 * f 1) = 0

case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : ∀ (n : ℕ), f (n * f 1) = n
⊢ f 1 = 1
Tactic:
replace this := congr_arg f (this (f 1))
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f (f (f 1 * f 1)) = f (f 1)
⊢ f 1 = 1

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f (f (f 1 * f 1)) = f (f 1)
⊢ f 1 = 1
Tactic:
rw [h0, h0] at this
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f 1 * f 1 = 1
⊢ f 1 = 1

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f 1 * f 1 = 1
⊢ f 1 = 1
Tactic:
exact Nat.eq_one_of_mul_eq_one_left this
State after:
no goals

State before:
case h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n_ih : ∀ m < 0, f (m * f 1) = m
⊢ f (0 * f 1) = 0
Tactic:
simp[h1]
State after:
no goals

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
replace h := h (n * f 1)
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f (n * f 1 + f 1) ≤ f (n * f 1) + 1
⊢ f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f (n * f 1 + f 1) ≤ f (n * f 1) + 1
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
rw [n_ih n n.lt_succ_self, ← add_one_mul, le_iff_eq_or_lt, Nat.lt_succ_iff] at h
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
revert h
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n → f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n → f ((n + 1) * f 1) = n + 1
Tactic:
refine (or_iff_left_of_imp (λ h ↦ ?_)).mp
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
replace n_ih := congr_arg f (n_ih _ (lt_of_le_of_lt h n.lt_succ_self))
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f (f (f ((n + 1) * f 1) * f 1)) = f (f ((n + 1) * f 1))
⊢ f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f (f (f ((n + 1) * f 1) * f 1)) = f (f ((n + 1) * f 1))
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
rw [h0, h0, mul_eq_mul_right_iff] at n_ih
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0
⊢ f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
revert n_ih
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0 → f ((n + 1) * f 1) = n + 1

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0 → f ((n + 1) * f 1) = n + 1
Tactic:
refine (or_iff_left ?_).mp
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = 0

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = 0
Tactic:
rw [← h1]
State after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = f 0

State before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = f 0
Tactic:
apply_fun f
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f (f 1) ≠ f (f 0)

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f (f 1) ≠ f (f 0)
Tactic:
rw [h0, h0]
State after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ 1 ≠ 0

State before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
State after:
no goals

State before:
case mpr.intro.intro.h.h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x_ih : ∀ m < 0, f m = m
⊢ f 0 = 0
Tactic:
exact h1
State after:
no goals