α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (Nat.gcd m n) x
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
revert hm hn
case refine'_1
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x

case refine'_2
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (Nat.gcd m n) x
refine' Nat.gcd.induction m n (fun n _ hn => _) fun m n _ ih hm hn => _
no goals
case refine'_1
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x
rwa [Nat.gcd_zero_left]
case refine'_2
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd (n % m) m) x
case refine'_2
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
rw [Nat.gcd_rec]
no goals
case refine'_2
α : Type u_1
β : Type ?u.3903
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd (n % m) m) x
exact ih (hn.mod hm) hm