Theorem: square_subset_square (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
p : ℂ
c₁ c₂ : ℝ
hc₁ : 0 < c₁
hc : c₁ ≤ c₂
⊢ Square p c₁ ⊆ Square p c₂
Tactic:
apply RectSubRect' <;> simpa using by linarith
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
c₁ c₂ : ℝ
hc₁ : 0 < c₁
hc : c₁ ≤ c₂
⊢ c₁ ≤ c₂
Tactic:
linarith
State after:
no goals