Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * 0 → P k
⊢ P (2 * 0)

pp: case succ.zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * (0 + 1) → P k
⊢ P (2 * (0 + 1))

pp: case succ.succ.zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * (0 + 1 + 1) → P k
⊢ P (2 * (0 + 1 + 1))

pp: case succ.succ.succ
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n n✝ : ℕ
h : (k : ℕ) → k < 2 * (n✝ + 1 + 1 + 1) → P k
⊢ P (2 * (n✝ + 1 + 1 + 1))

Tactic:
;

Goal state after:
case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * 0 → P k
⊢ P (2 * 0)

case succ.zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * (0 + 1) → P k
⊢ P (2 * (0 + 1))

case succ.succ.zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * (0 + 1 + 1) → P k
⊢ P (2 * (0 + 1 + 1))

case succ.succ.succ
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n n✝ : ℕ
h : (k : ℕ) → k < 2 * (n✝ + 1 + 1 + 1) → P k
⊢ P (2 * (n✝ + 1 + 1 + 1))