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
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
contrapose! fg
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
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
let fmin : A := f.support.min' (support_nonempty_iff.mpr fg.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)
⊢ Finset.Nonempty (f * g).support
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
refine' support_nonempty_iff.mp _
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 ?m.36783
⊢ Finset.Nonempty (f * g).support
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
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 _ _)
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
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 ?m.36783
⊢ Finset.Nonempty (f * g).support
refine' ⟨fmin + a, mem_support_iff.mpr _⟩
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

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
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
rw [mul_apply_add_eq_mul_of_forall_ne _]
no goals
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
rw [support_single_mul] <;> simp [support_nonempty_iff.mpr fg.2]
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
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
refine' mul_ne_zero _ _
no goals
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
exacts [mem_support_iff.mp (Finset.min'_mem _ _), mem_support_iff.mp 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)
⊢ ∀ {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)
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
rw [H]
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

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
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)
rintro b c bf cg (hb | hc) <;> refine' ne_of_gt _
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

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
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
refine' lt_of_le_of_lt (_ : _ ≤ fmin + c) _
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
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
apply Finset.min'_le
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
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
rw [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _)]
no goals
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
simp only [cg, Finset.mem_map, addLeftEmbedding_apply, add_right_inj, exists_prop,
  exists_eq_right]
no goals
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
rw [one_mul]
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
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
refine' add_lt_add_right _ _
no goals
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
exact Finset.min'_lt_of_mem_erase_min' _ _ (Finset.mem_erase.mpr ⟨hb, bf⟩)
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

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
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
refine' lt_of_lt_of_le (_ : _ < fmin + c) _
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))
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
apply Finset.min'_lt_of_mem_erase_min'
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)
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))
rw [← H]
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

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
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)
apply Finset.mem_erase_of_ne_of_mem
no goals
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
simpa only [Ne.def, add_right_inj]
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
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
rw [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _)]
no goals
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
simpa only [Finset.mem_map, addLeftEmbedding_apply, add_right_inj, exists_prop,
  exists_eq_right]
no goals
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
rw [one_mul]
no goals
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
exact add_le_add_right (Finset.min'_le _ _ bf) _