Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a + coeff y a ≠ 0
⊢ a ∈ support x ∪ support y
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : a ∈ support (x + y)
⊢ a ∈ support x ∪ support y
rw [mem_support, add_coeff] at ha
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a + coeff y a ≠ 0
⊢ coeff x a ≠ 0 ∨ coeff y a ≠ 0
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a + coeff y a ≠ 0
⊢ a ∈ support x ∪ support y
rw [Set.mem_union, mem_support, mem_support]
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a = 0 ∧ coeff y a = 0
⊢ coeff x a + coeff y a = 0
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a + coeff y a ≠ 0
⊢ coeff x a ≠ 0 ∨ coeff y a ≠ 0
contrapose! ha
no goals
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : coeff x a = 0 ∧ coeff y a = 0
⊢ coeff x a + coeff y a = 0
rw [ha.1, ha.2, add_zero]