case intro
F : Type ?u.192927
α : Type ?u.192930
β : Type ?u.192933
γ : Type ?u.192936
R : Type u_1
S : Type u_2
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f (s ^ 2)
F : Type ?u.192927
α : Type ?u.192930
β : Type ?u.192933
γ : Type ?u.192936
R : Type u_1
S : Type u_2
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
r : R
h : 0 ≤ r
⊢ 0 ≤ ↑f r
obtain ⟨s, rfl⟩ := hR r h
case intro
F : Type ?u.192927
α : Type ?u.192930
β : Type ?u.192933
γ : Type ?u.192936
R : Type u_1
S : Type u_2
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f s ^ 2
case intro
F : Type ?u.192927
α : Type ?u.192930
β : Type ?u.192933
γ : Type ?u.192936
R : Type u_1
S : Type u_2
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f (s ^ 2)
rw [map_pow]
no goals
case intro
F : Type ?u.192927
α : Type ?u.192930
β : Type ?u.192933
γ : Type ?u.192936
R : Type u_1
S : Type u_2
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f s ^ 2
apply sq_nonneg