case inl
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = a
⊢ Even (abs a) ↔ Even a

case inr
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = -a
⊢ Even (abs a) ↔ Even a
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
⊢ Even (abs a) ↔ Even a
cases abs_choice a
case inl
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : abs a = a
⊢ Even (abs a) ↔ Even a
case inl
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = a
⊢ Even (abs a) ↔ Even a
have h : abs a = a := by assumption
no goals
case inl
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : abs a = a
⊢ Even (abs a) ↔ Even a
simp only [h, even_neg]
no goals
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = a
⊢ abs a = a
assumption
case inr
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : abs a = -a
⊢ Even (abs a) ↔ Even a
case inr
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = -a
⊢ Even (abs a) ↔ Even a
have h : abs a = -a := by assumption
no goals
case inr
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : abs a = -a
⊢ Even (abs a) ↔ Even a
simp only [h, even_neg]
no goals
F : Type ?u.48526
α : Type u_1
β : Type ?u.48532
R : Type ?u.48535
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : abs a = -a
⊢ abs a = -a
assumption