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

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
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
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✝² : 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
rw [support_mul_single] <;> simp [support_nonempty_iff.mpr fg.1]
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
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
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✝² : 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
exacts [mem_support_iff.mp ha, mem_support_iff.mp (Finset.min'_mem _ _)]
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)
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
rw [H]
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

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
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)
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✝² : 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

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

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
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)
apply Finset.mem_erase_of_ne_of_mem
no goals
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
simpa only [Ne.def, add_left_inj]
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
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
rw [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _)]
no goals
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
simpa only [Finset.mem_map, addRightEmbedding_apply, add_left_inj, exists_prop,
  exists_eq_right]
no goals
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
rw [mul_one]
no goals
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
exact add_le_add_left (Finset.min'_le _ _ cg) _
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

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
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
refine' lt_of_le_of_lt (_ : _ ≤ b + gmin) _
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
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
apply Finset.min'_le
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
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
rw [support_mul_single _ _ (fun y => by rw [mul_one] : ∀ y : R, y * 1 = 0 ↔ _)]
no goals
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
simp only [bf, Finset.mem_map, addRightEmbedding_apply, add_left_inj, exists_prop,
  exists_eq_right]
no goals
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
rw [mul_one]
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
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
refine' add_lt_add_left _ _
no goals
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
exact Finset.min'_lt_of_mem_erase_min' _ _ (Finset.mem_erase.mpr ⟨hc, cg⟩)