case inl
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

case inr
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x
cases' le_total n m with h h
case inl
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x
case inl
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x
refine' left_of_add _ hn
no goals
case inl
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x
rwa [tsub_add_cancel_of_le h]
case inr
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x
case inr
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
rw [tsub_eq_zero_iff_le.mpr h]
no goals
case inr
α : Type u_1
β : Type ?u.1528
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x
apply isPeriodicPt_zero