Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 1)

pp: case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 2)

pp: case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 3)

pp: case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 4)

Tactic:
<;>

Goal state after:
case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 1)

case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 2)

case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 3)

case a
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (x✝ + 4)