case mp
x✝ y x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

case mpr
x✝ y x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
x✝ y x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
constructor
case mp
x✝ y x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
case mp
x✝ y x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
intro h
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

case mp.inr.inl
x y : ℝ
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1

case mp.inr.inr
x✝ y x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1
case mp
x✝ y x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
refine' Or.inr (Or.inr (neg_eq_iff_eq_neg.mp _))
case mp.inl
x✝ y x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
rw [← log_neg_eq_log x] at h
no goals
case mp.inl
x✝ y x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h
no goals
case mp.inr.inl
x y : ℝ
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1
exact Or.inl rfl
no goals
case mp.inr.inr
x✝ y x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1
exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))
no goals
case mpr
x✝ y x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
rintro (rfl | rfl | rfl) <;> simp only [log_one, log_zero, log_neg_eq_log]