Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ Set.IsPwo (support x)

Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ Set.IsPwo (support y)

Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ∀ (x_1 : Γ), x_1 ∈ support (x * y) → x_1 ∈ {a | Finset.Nonempty (addAntidiagonal ?m.1223652 ?m.1223653 a)}
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ support (x * y) ⊆ support x + support y
apply Set.Subset.trans (fun x hx => _) support_addAntidiagonal_subset_add
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : x ∈ support (x✝ * y)
⊢ x ∈ {a | Finset.Nonempty (addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) a)}
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ∀ (x_1 : Γ),
    x_1 ∈ support (x * y) →
      x_1 ∈ {a | Finset.Nonempty (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a)}
intro x hx
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : ¬x ∈ {a | Finset.Nonempty (addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) a)}
⊢ ¬x ∈ support (x✝ * y)
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : x ∈ support (x✝ * y)
⊢ x ∈ {a | Finset.Nonempty (addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) a)}
contrapose! hx
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) x = ∅
⊢ ¬x ∈ support (x✝ * y)
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : ¬x ∈ {a | Finset.Nonempty (addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) a)}
⊢ ¬x ∈ support (x✝ * y)
simp only [not_nonempty_iff_eq_empty, Ne.def, Set.mem_setOf_eq] at hx
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x✝ y : HahnSeries Γ R
x : Γ
hx : addAntidiagonal (_ : Set.IsPwo (support x✝)) (_ : Set.IsPwo (support y)) x = ∅
⊢ ¬x ∈ support (x✝ * y)
simp [hx, mul_coeff]
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ Set.IsPwo (support x)
exact x.isPwo_support
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ Set.IsPwo (support y)
exact y.isPwo_support