𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ ↑x = ↑y ↔ x = y
refine' ⟨fun h => _, by tauto⟩
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y
suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
apply_fun equivIco p a  at h
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := x, property := hx }) =
    Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := y, property := hy })
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
no goals
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := x, property := hx }) =
    Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := y, property := hy })
exact h
no goals
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ x = y → ↑x = ↑y
tauto
no goals
𝕜 : Type u_1
B : Type ?u.79444
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
this : { val := x, property := hx } = { val := y, property := hy }
⊢ x = y
exact Subtype.mk.inj this