case mk
𝕜 : Type ?u.337557
B : Type ?u.337560
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ restrict (Icc a (a + p)) f { val := a, property := (_ : a ∈ Icc a (a + p)) } =
    restrict (Icc a (a + p)) f { val := a + p, property := (_ : a + p ∈ Icc a (a + p)) }
𝕜 : Type ?u.337557
B : Type ?u.337560
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b
rintro _ _ ⟨_⟩
no goals
case mk
𝕜 : Type ?u.337557
B : Type ?u.337560
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ restrict (Icc a (a + p)) f { val := a, property := (_ : a ∈ Icc a (a + p)) } =
    restrict (Icc a (a + p)) f { val := a + p, property := (_ : a + p ∈ Icc a (a + p)) }
exact h