case intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : α
hn : Even n
a : α
⊢ Even (a + a - n)
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)
obtain ⟨a, rfl⟩ := hm
case intro.intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ Even (a + a - (b + b))
case intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : α
hn : Even n
a : α
⊢ Even (a + a - n)
obtain ⟨b, rfl⟩ := hn
case intro.intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a + a - (b + b) = a - b + (a - b)
case intro.intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ Even (a + a - (b + b))
refine' ⟨a - b, _⟩
case intro.intro.inl
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

case intro.intro.inr
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
case intro.intro
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a + a - (b + b) = a - b + (a - b)
obtain h | h := le_total a b
no goals
case intro.intro.inl
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
no goals
case intro.intro.inr
F : Type ?u.56414
α : Type u_1
β : Type ?u.56420
R : Type ?u.56423
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
exact (tsub_add_tsub_comm h h).symm