Theorem: TrussDesign.wminₚ_le_wmaxₚ (CvxLean/Examples/TrussDesign.lean)

State before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ wminₚ ≤ wmaxₚ
Tactic:
unfold wminₚ wmaxₚ
State after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100

State before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100
Tactic:
norm_num
State after:
no goals