[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ↑(f * g) (a0 + b0) = ↑f a0 * ↑g b0
[PROOFSTEP]
classical
rw [mul_apply]
refine' (Finset.sum_eq_single a0 _ _).trans _
· exact fun b H hb => Finset.sum_eq_zero fun x H1 => if_neg (h H H1 (Or.inl hb))
· exact fun af0 => by simp [not_mem_support_iff.mp af0]
· refine' (Finset.sum_eq_single b0 (fun b bg b0 => _) _).trans (if_pos rfl)
  · by_cases af : a0 ∈ f.support
    · exact if_neg (h af bg (Or.inr b0))
    · simp only [not_mem_support_iff.mp af, zero_mul, ite_self]
  · exact fun bf0 => by simp [not_mem_support_iff.mp bf0]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ↑(f * g) (a0 + b0) = ↑f a0 * ↑g b0
[PROOFSTEP]
rw [mul_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) = ↑f a0 * ↑g b0
[PROOFSTEP]
refine' (Finset.sum_eq_single a0 _ _).trans _
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ∀ (b : A),
    b ∈ f.support → b ≠ a0 → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) b (↑f b) = 0
[PROOFSTEP]
exact fun b H hb => Finset.sum_eq_zero fun x H1 => if_neg (h H H1 (Or.inl hb))
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬a0 ∈ f.support → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = 0
[PROOFSTEP]
exact fun af0 => by simp [not_mem_support_iff.mp af0]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
af0 : ¬a0 ∈ f.support
⊢ (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = 0
[PROOFSTEP]
simp [not_mem_support_iff.mp af0]
[GOAL]
case refine'_3
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = ↑f a0 * ↑g b0
[PROOFSTEP]
refine' (Finset.sum_eq_single b0 (fun b bg b0 => _) _).trans (if_pos rfl)
[GOAL]
case refine'_3.refine'_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
[PROOFSTEP]
by_cases af : a0 ∈ f.support
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
[PROOFSTEP]
exact if_neg (h af bg (Or.inr b0))
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : ¬a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
[PROOFSTEP]
simp only [not_mem_support_iff.mp af, zero_mul, ite_self]
[GOAL]
case refine'_3.refine'_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬b0 ∈ g.support → (fun a₂ b₂ => if a0 + a₂ = a0 + b0 then ↑f a0 * b₂ else 0) b0 (↑g b0) = 0
[PROOFSTEP]
exact fun bf0 => by simp [not_mem_support_iff.mp bf0]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
bf0 : ¬b0 ∈ g.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0 then ↑f a0 * b₂ else 0) b0 (↑g b0) = 0
[PROOFSTEP]
simp [not_mem_support_iff.mp bf0]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : AddLeftCancelSemigroup A
g : AddMonoidAlgebra R A
a x : A
hx : x ∈ (single a 1 * g).support
⊢ ∃ b, b ∈ g.support ∧ a + b = x
[PROOFSTEP]
rwa [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _), Finset.mem_map] at hx 
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : AddLeftCancelSemigroup A
g : AddMonoidAlgebra R A
a x : A
hx : x ∈ (single a 1 * g).support
y : R
⊢ 1 * y = 0 ↔ y = 0
[PROOFSTEP]
rw [one_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : AddRightCancelSemigroup A
f : AddMonoidAlgebra R A
b x : A
hx : x ∈ (f * single b 1).support
⊢ ∃ a, a ∈ f.support ∧ a + b = x
[PROOFSTEP]
rwa [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _), Finset.mem_map] at hx 
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : AddRightCancelSemigroup A
f : AddMonoidAlgebra R A
b x : A
hx : x ∈ (f * single b 1).support
y : R
⊢ y * 1 = 0 ↔ y = 0
[PROOFSTEP]
rw [mul_one]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f * g = 0
⊢ f = 0 ∨ g = 0
[PROOFSTEP]
contrapose! fg
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
⊢ f * g ≠ 0
[PROOFSTEP]
let gmin : A := g.support.min' (support_nonempty_iff.mpr fg.2)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
⊢ f * g ≠ 0
[PROOFSTEP]
refine' support_nonempty_iff.mp _
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
⊢ Finset.Nonempty (f * g).support
[PROOFSTEP]
obtain ⟨a, ha, H⟩ :=
  Right.exists_add_of_mem_support_single_mul gmin
    ((f * single gmin 1 : AddMonoidAlgebra R A).support.min'
      (by rw [support_mul_single] <;> simp [support_nonempty_iff.mpr fg.1]))
    (Finset.min'_mem _ _)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
⊢ Finset.Nonempty (f * single gmin 1).support
[PROOFSTEP]
rw [support_mul_single]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
⊢ Finset.Nonempty (Finset.map (addRightEmbedding gmin) f.support)
[PROOFSTEP]
simp [support_nonempty_iff.mpr fg.1]
[GOAL]
case hr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
⊢ ∀ (y : R), y * 1 = 0 ↔ y = 0
[PROOFSTEP]
simp [support_nonempty_iff.mpr fg.1]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ Finset.Nonempty (f * g).support
[PROOFSTEP]
refine' ⟨a + gmin, mem_support_iff.mpr _⟩
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ↑(f * g) (a + gmin) ≠ 0
[PROOFSTEP]
rw [mul_apply_add_eq_mul_of_forall_ne _]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ↑f a * ↑g gmin ≠ 0
[PROOFSTEP]
refine' mul_ne_zero _ _
[GOAL]
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ↑f a ≠ 0
case intro.intro.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ↑g gmin ≠ 0
[PROOFSTEP]
exacts [mem_support_iff.mp ha, mem_support_iff.mp (Finset.min'_mem _ _)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ∀ {a_1 b : A}, a_1 ∈ f.support → b ∈ g.support → a_1 ≠ a ∨ b ≠ gmin → a_1 + b ≠ a + gmin
[PROOFSTEP]
rw [H]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
⊢ ∀ {a_1 b : A},
    a_1 ∈ f.support →
      b ∈ g.support →
        a_1 ≠ a ∨ b ≠ gmin →
          a_1 + b ≠ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
[PROOFSTEP]
rintro b c bf cg (hb | hc)
[GOAL]
case inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + c ≠ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
[PROOFSTEP]
refine' ne_of_gt _
[GOAL]
case inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ b + c ≠ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
[PROOFSTEP]
refine' ne_of_gt _
[GOAL]
case inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support) < b + c
[PROOFSTEP]
refine' lt_of_lt_of_le (_ : _ < b + gmin) _
[GOAL]
case inl.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support) < b + gmin
[PROOFSTEP]
apply Finset.min'_lt_of_mem_erase_min'
[GOAL]
case inl.refine'_1.ha
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ∈
    Finset.erase (f * single gmin 1).support
      (Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support))
[PROOFSTEP]
rw [← H]
[GOAL]
case inl.refine'_1.ha
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ∈ Finset.erase (f * single gmin 1).support (a + gmin)
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem
[GOAL]
case inl.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ≠ a + gmin
[PROOFSTEP]
simpa only [Ne.def, add_left_inj]
[GOAL]
case inl.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ∈ (f * single gmin 1).support
[PROOFSTEP]
rw [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
y : R
⊢ y * 1 = 0 ↔ y = 0
[PROOFSTEP]
rw [mul_one]
[GOAL]
case inl.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ∈ Finset.map (addRightEmbedding gmin) f.support
[PROOFSTEP]
simpa only [Finset.mem_map, addRightEmbedding_apply, add_left_inj, exists_prop, exists_eq_right]
[GOAL]
case inl.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
⊢ b + gmin ≤ b + c
[PROOFSTEP]
haveI : CovariantClass A A (· + ·) (· ≤ ·) := Add.to_covariantClass_left A
[GOAL]
case inl.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ a
this : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b + gmin ≤ b + c
[PROOFSTEP]
exact add_le_add_left (Finset.min'_le _ _ cg) _
[GOAL]
case inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support) < b + c
[PROOFSTEP]
refine' lt_of_le_of_lt (_ : _ ≤ b + gmin) _
[GOAL]
case inr.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support) ≤ b + gmin
[PROOFSTEP]
apply Finset.min'_le
[GOAL]
case inr.refine'_1.H2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ b + gmin ∈ (f * single gmin 1).support
[PROOFSTEP]
rw [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
y : R
⊢ y * 1 = 0 ↔ y = 0
[PROOFSTEP]
rw [mul_one]
[GOAL]
case inr.refine'_1.H2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ b + gmin ∈ Finset.map (addRightEmbedding gmin) f.support
[PROOFSTEP]
simp only [bf, Finset.mem_map, addRightEmbedding_apply, add_left_inj, exists_prop, exists_eq_right]
[GOAL]
case inr.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ b + gmin < b + c
[PROOFSTEP]
refine' add_lt_add_left _ _
[GOAL]
case inr.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddRightCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
gmin : A := Finset.min' g.support (_ : Finset.Nonempty g.support)
a : A
ha : a ∈ f.support
H : a + gmin = Finset.min' (f * single gmin 1).support (_ : Finset.Nonempty (f * single gmin 1).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ gmin
⊢ gmin < c
[PROOFSTEP]
exact Finset.min'_lt_of_mem_erase_min' _ _ (Finset.mem_erase.mpr ⟨hc, cg⟩)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f * g = 0
⊢ f = 0 ∨ g = 0
[PROOFSTEP]
contrapose! fg
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
⊢ f * g ≠ 0
[PROOFSTEP]
let fmin : A := f.support.min' (support_nonempty_iff.mpr fg.1)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
⊢ f * g ≠ 0
[PROOFSTEP]
refine' support_nonempty_iff.mp _
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
⊢ Finset.Nonempty (f * g).support
[PROOFSTEP]
obtain ⟨a, ha, H⟩ :=
  Left.exists_add_of_mem_support_single_mul fmin
    ((single fmin 1 * g : AddMonoidAlgebra R A).support.min'
      (by rw [support_single_mul] <;> simp [support_nonempty_iff.mpr fg.2]))
    (Finset.min'_mem _ _)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
⊢ Finset.Nonempty (single fmin 1 * g).support
[PROOFSTEP]
rw [support_single_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
⊢ Finset.Nonempty (Finset.map (addLeftEmbedding fmin) g.support)
[PROOFSTEP]
simp [support_nonempty_iff.mpr fg.2]
[GOAL]
case hr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
⊢ ∀ (y : R), 1 * y = 0 ↔ y = 0
[PROOFSTEP]
simp [support_nonempty_iff.mpr fg.2]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ Finset.Nonempty (f * g).support
[PROOFSTEP]
refine' ⟨fmin + a, mem_support_iff.mpr _⟩
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ↑(f * g) (fmin + a) ≠ 0
[PROOFSTEP]
rw [mul_apply_add_eq_mul_of_forall_ne _]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ↑f fmin * ↑g a ≠ 0
[PROOFSTEP]
refine' mul_ne_zero _ _
[GOAL]
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ↑f fmin ≠ 0
case intro.intro.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ↑g a ≠ 0
[PROOFSTEP]
exacts [mem_support_iff.mp (Finset.min'_mem _ _), mem_support_iff.mp ha]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ∀ {a_1 b : A}, a_1 ∈ f.support → b ∈ g.support → a_1 ≠ fmin ∨ b ≠ a → a_1 + b ≠ fmin + a
[PROOFSTEP]
rw [H]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
⊢ ∀ {a_1 b : A},
    a_1 ∈ f.support →
      b ∈ g.support →
        a_1 ≠ fmin ∨ b ≠ a →
          a_1 + b ≠ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
[PROOFSTEP]
rintro b c bf cg (hb | hc)
[GOAL]
case inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ b + c ≠ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
[PROOFSTEP]
refine' ne_of_gt _
[GOAL]
case inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ b + c ≠ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
[PROOFSTEP]
refine' ne_of_gt _
[GOAL]
case inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support) < b + c
[PROOFSTEP]
refine' lt_of_le_of_lt (_ : _ ≤ fmin + c) _
[GOAL]
case inl.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support) ≤ fmin + c
[PROOFSTEP]
apply Finset.min'_le
[GOAL]
case inl.refine'_1.H2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ fmin + c ∈ (single fmin 1 * g).support
[PROOFSTEP]
rw [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
y : R
⊢ 1 * y = 0 ↔ y = 0
[PROOFSTEP]
rw [one_mul]
[GOAL]
case inl.refine'_1.H2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ fmin + c ∈ Finset.map (addLeftEmbedding fmin) g.support
[PROOFSTEP]
simp only [cg, Finset.mem_map, addLeftEmbedding_apply, add_right_inj, exists_prop, exists_eq_right]
[GOAL]
case inl.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ fmin + c < b + c
[PROOFSTEP]
refine' add_lt_add_right _ _
[GOAL]
case inl.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hb : b ≠ fmin
⊢ fmin < b
[PROOFSTEP]
exact Finset.min'_lt_of_mem_erase_min' _ _ (Finset.mem_erase.mpr ⟨hb, bf⟩)
[GOAL]
case inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support) < b + c
[PROOFSTEP]
refine' lt_of_lt_of_le (_ : _ < fmin + c) _
[GOAL]
case inr.refine'_1
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support) < fmin + c
[PROOFSTEP]
apply Finset.min'_lt_of_mem_erase_min'
[GOAL]
case inr.refine'_1.ha
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ∈
    Finset.erase (single fmin 1 * g).support
      (Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support))
[PROOFSTEP]
rw [← H]
[GOAL]
case inr.refine'_1.ha
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ∈ Finset.erase (single fmin 1 * g).support (fmin + a)
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem
[GOAL]
case inr.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ≠ fmin + a
[PROOFSTEP]
simpa only [Ne.def, add_right_inj]
[GOAL]
case inr.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ∈ (single fmin 1 * g).support
[PROOFSTEP]
rw [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _)]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
y : R
⊢ 1 * y = 0 ↔ y = 0
[PROOFSTEP]
rw [one_mul]
[GOAL]
case inr.refine'_1.ha.a
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ∈ Finset.map (addLeftEmbedding fmin) g.support
[PROOFSTEP]
simpa only [Finset.mem_map, addLeftEmbedding_apply, add_right_inj, exists_prop, exists_eq_right]
[GOAL]
case inr.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
⊢ fmin + c ≤ b + c
[PROOFSTEP]
haveI : CovariantClass A A (Function.swap (· + ·)) (· ≤ ·) := Add.to_covariantClass_right A
[GOAL]
case inr.refine'_2
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : NoZeroDivisors R
inst✝² : AddLeftCancelSemigroup A
inst✝¹ : LinearOrder A
inst✝ : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
f g : AddMonoidAlgebra R A
fg : f ≠ 0 ∧ g ≠ 0
fmin : A := Finset.min' f.support (_ : Finset.Nonempty f.support)
a : A
ha : a ∈ g.support
H : fmin + a = Finset.min' (single fmin 1 * g).support (_ : Finset.Nonempty (single fmin 1 * g).support)
b c : A
bf : b ∈ f.support
cg : c ∈ g.support
hc : c ≠ a
this : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ fmin + c ≤ b + c
[PROOFSTEP]
exact add_le_add_right (Finset.min'_le _ _ bf) _
