case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : r = 0
⊢ coeff (x * ↑(single b) r) (a + b) = coeff x a * r

case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ coeff (x * ↑(single b) r) (a + b) = coeff x a * r
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
⊢ coeff (x * ↑(single b) r) (a + b) = coeff x a * r
by_cases hr : r = 0
case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r
case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ coeff (x * ↑(single b) r) (a + b) = coeff x a * r
simp only [hr, smul_coeff, mul_coeff, support_single_of_ne, Ne.def, not_false_iff, smul_eq_mul]
case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r

case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r
case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r
by_cases hx : x.coeff a = 0
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    ∑ ij in {(a, b)}, coeff x ij.fst * coeff (↑(single b) r) ij.snd

Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ ij in {(a, b)}, coeff x ij.fst * coeff (↑(single b) r) ij.snd = coeff x a * r
case neg
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r
trans ∑ ij : Γ × Γ in {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd
no goals
case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : r = 0
⊢ coeff (x * ↑(single b) r) (a + b) = coeff x a * r
simp [hr, mul_coeff]
case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    0
case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    coeff x a * r
simp only [hx, MulZeroClass.zero_mul]
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) = ∅
case pos
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    0
rw [sum_congr _ fun _ _ => rfl, sum_empty]
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) ↔ (a1, a2) ∈ ∅
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
⊢ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) = ∅
ext ⟨a1, a2⟩
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x → a2 = b → ¬a1 + a2 = a + b
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) ↔ (a1, a2) ∈ ∅
simp only [not_mem_empty, not_and, Set.mem_singleton_iff, Classical.not_not,
  mem_addAntidiagonal, Set.mem_setOf_eq, iff_false_iff]
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
h2 : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ False
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x → a2 = b → ¬a1 + a2 = a + b
rintro h2 rfl h1
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
a1 : Γ
hx : coeff x a1 = 0
a2 : Γ
h2 : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ False
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : coeff x a = 0
a1 a2 : Γ
h2 : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ False
rw [← add_right_cancel h1] at hx
no goals
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
a1 : Γ
hx : coeff x a1 = 0
a2 : Γ
h2 : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ False
exact h2 hx
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) = {(a, b)}
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ x_1 in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b),
      coeff x x_1.fst * coeff (↑(single b) r) x_1.snd =
    ∑ ij in {(a, b)}, coeff x ij.fst * coeff (↑(single b) r) ij.snd
apply sum_congr _ fun _ _ => rfl
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) ↔ (a1, a2) ∈ {(a, b)}
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) = {(a, b)}
ext ⟨a1, a2⟩
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo {b}) (a + b) ↔ (a1, a2) ∈ {(a, b)}
simp only [Set.mem_singleton_iff, Prod.mk.inj_iff, mem_addAntidiagonal, mem_singleton,
  Set.mem_setOf_eq]
case a.mk.mp
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b

case a.mk.mpr
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 = a ∧ a2 = b → a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b
case a.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b
constructor
case a.mk.mp.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
left✝ : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2
case a.mk.mp
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b
rintro ⟨_, rfl, h1⟩
no goals
case a.mk.mp.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
left✝ : a1 ∈ support x
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2
refine' ⟨add_right_cancel h1, rfl⟩
case a.mk.mpr.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
hr : ¬r = 0
a1 a2 : Γ
hx : ¬coeff x a1 = 0
⊢ a1 ∈ support x ∧ a2 = a2 ∧ a1 + a2 = a1 + a2
case a.mk.mpr
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
a1 a2 : Γ
⊢ a1 = a ∧ a2 = b → a1 ∈ support x ∧ a2 = b ∧ a1 + a2 = a + b
rintro ⟨rfl, rfl⟩
no goals
case a.mk.mpr.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
hr : ¬r = 0
a1 a2 : Γ
hx : ¬coeff x a1 = 0
⊢ a1 ∈ support x ∧ a2 = a2 ∧ a1 + a2 = a1 + a2
simp [hx]
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬coeff x a = 0
⊢ ∑ ij in {(a, b)}, coeff x ij.fst * coeff (↑(single b) r) ij.snd = coeff x a * r
simp