case mp
x y : ℝ
⊢ sqrt x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → sqrt x = y
x y : ℝ
⊢ sqrt x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
constructor
case mp
x : ℝ
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
case mp
x y : ℝ
⊢ sqrt x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
rintro rfl
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0

case mp.inr
x : ℝ
hlt : x < 0
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
case mp
x : ℝ
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
cases' le_or_lt 0 x with hle hlt
no goals
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
no goals
case mp.inr
x : ℝ
hlt : x < 0
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ sqrt (y * y) = y

case mpr.inr.intro
x : ℝ
hx : x < 0
⊢ sqrt x = 0
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → sqrt x = y
rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
no goals
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ sqrt (y * y) = y

case mpr.inr.intro
x : ℝ
hx : x < 0
⊢ sqrt x = 0
exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]