Theorem: max_ne_self_iff (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬a = max a b ↔ a < b
Tactic:
rw [max_def]
State after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ (¬a = if a ≤ b then b else a) ↔ a < b

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ (¬a = if a ≤ b then b else a) ↔ a < b
Tactic:
split_ifs with h
State after:
case pos
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : a ≤ b
⊢ ¬a = b ↔ a < b

case neg
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : ¬a ≤ b
⊢ ¬a = a ↔ a < b

State before:
case pos
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : a ≤ b
⊢ ¬a = b ↔ a < b
Tactic:
simpa using h
State after:
no goals

State before:
case neg
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : ¬a ≤ b
⊢ ¬a = a ↔ a < b
Tactic:
simpa using le_of_not_ge h
State after:
no goals