Theorem: iterate_left (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ {A : Sort u_1} (f : A → A) (n : ℕ) (x : A), f^[n + 1] x = f (f^[n] x)
Tactic:
intros A f n
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
⊢ ∀ (x : A), f^[n + 1] x = f (f^[n] x)

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
⊢ ∀ (x : A), f^[n + 1] x = f (f^[n] x)
Tactic:
induction' n with n ihn
State after:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)

case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)

State before:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)

case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
. simp [Nat.iterate]
State after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)

State before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
. simp [Nat.add, Nat.iterate]
  intros x
  apply ihn
State after:
no goals

State before:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)
Tactic:
simp [Nat.iterate]
State after:
no goals

State before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
simp [Nat.add, Nat.iterate]
State after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[n] (f (f x)) = f (f^[n] (f x))

State before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[n] (f (f x)) = f (f^[n] (f x))
Tactic:
intros x
State after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
x : A
⊢ f^[n] (f (f x)) = f (f^[n] (f x))

State before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
x : A
⊢ f^[n] (f (f x)) = f (f^[n] (f x))
Tactic:
apply ihn
State after:
no goals