awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
this :
  ∀ {mn : M × N} {r : R},
    Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul f = (AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f
have hfg : ∀ (m₁ : M) (n₁ : N) (r₁ : R) (m₂ : M) (n₂ : N) (r₂ : R) (m : M) (m_1 : N),
  Eq.{u_1 + 1} (α := R)
    ((((((AddMonoidHom.comp
                        (((AddMonoidHom.compr₂ AddMonoidHom.mul f).comp (singleAddHom (m₁, n₁)) :
                            (a : R) → R[M × N] →+ R[N][M])
                          r₁)
                        (singleAddHom (m₂, n₂)) :
                      (a : R) → R[N][M])
                    r₂ :
                  R[N][M]) :
                (a : M) → R[N])
              m :
            R[N]) :
          (a : N) → R)
        m_1 :
      R)
    ((((((AddMonoidHom.comp
                        ((((AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f).comp (singleAddHom (m₁, n₁)) :
                            (a : R) → R[M × N] →+ R[N][M])
                          r₁)
                        (singleAddHom (m₂, n₂)) :
                      (a : R) → R[N][M])
                    r₂ :
                  R[N][M]) :
                (a : M) → R[N])
              m :
            R[N]) :
          (a : N) → R)
        m_1 :
      R)
Tactic: ext ⟨m₁, n₁⟩ r₁ ⟨m₂, n₂⟩ r₂
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)
have rw : Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
  (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
Tactic: rw [mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq.{u_1 + 1} (α := R)
    (∑ a ∈ x.support,
      ∑ a_1 ∈ y.support,
        if a * a_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) a_1 : R) else 0)
    (∑ a ∈ x.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) (a⁻¹ * g) : R))
have a : ∀ x_1 ∈ x.support,
  (∑ a ∈ y.support,
      if x_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) a : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) (x_1⁻¹ * g) : R)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)
have rw : Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
  (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
Tactic: classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw rw₁ rw₂ :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)
have rw₃ : Eq.{u_1 + 1} (α := R)
  (∑ a ∈ x.support,
    ∑ a_1 ∈ y.support,
      if a * a_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) a_1 : R) else 0)
  (∑ a ∈ x.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) (a⁻¹ * g) : R))
Tactic: classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw rw₁ rw₂ :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
rw₃ :
  Eq.{u_1 + 1} (α := R)
    (∑ a ∈ x.support,
      ∑ a_1 ∈ y.support,
        if a * a_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) a_1 : R) else 0)
    (∑ a ∈ x.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) (a⁻¹ * g) : R))
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)
have a : ∀ x_1 ∈ x.support,
  (∑ a ∈ y.support,
      if x_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) a : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) (x_1⁻¹ * g) : R)
Tactic: classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)
have rw : Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
  (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
Tactic: rw [mul_apply, Finsupp.sum_comm]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq.{u_1 + 1} (α := R)
    (∑ a ∈ y.support,
      ∑ a_1 ∈ x.support,
        if a_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a_1 : R) ((y : (a : G) → R) a : R) else 0)
    (∑ a ∈ y.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * a⁻¹) : R) ((y : (a : G) → R) a : R))
have a : ∀ x_1 ∈ y.support,
  (∑ a ∈ x.support,
      if a * x_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) x_1 : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * x_1⁻¹) : R) ((y : (a : G) → R) x_1 : R)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)
have rw : Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
  (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
Tactic: classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)
have rw₁ : Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
  (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
Tactic: classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
rw₁ rw₂ rw₃ :
  Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)
have rw₄ : Eq.{u_1 + 1} (α := R)
  (∑ a ∈ y.support,
    ∑ a_1 ∈ x.support,
      if a_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a_1 : R) ((y : (a : G) → R) a : R) else 0)
  (∑ a ∈ y.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * a⁻¹) : R) ((y : (a : G) → R) a : R))
Tactic: classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
rw₁ rw₂ rw₃ :
  Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
rw₄ :
  Eq.{u_1 + 1} (α := R)
    (∑ a ∈ y.support,
      ∑ a_1 ∈ x.support,
        if a_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a_1 : R) ((y : (a : G) → R) a : R) else 0)
    (∑ a ∈ y.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * a⁻¹) : R) ((y : (a : G) → R) a : R))
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)
have a : ∀ x_1 ∈ y.support,
  (∑ a ∈ x.support,
      if a * x_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) x_1 : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * x_1⁻¹) : R) ((y : (a : G) → R) x_1 : R)
Tactic: classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
have rw : HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
  single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
Tactic: rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
rw :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
have rw₁ : HMul.hMul (α := R[M]) (single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i)) =
  single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
Tactic: rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
rw :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₁ :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
have rw₂ : Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
  (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
Tactic: rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
rw :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₁ :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₂ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
    (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
have rw₃ : Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i)) (single (m i * ∏ x ∈ s, m x) (∏ i ∈ cons i s hi, r i))
Tactic: rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
rw :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₁ :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₂ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
    (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
rw₃ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
    (single (m i * ∏ x ∈ s, m x) (∏ i ∈ cons i s hi, r i))
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
have rw₄ : Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i)) (single (m i * ∏ x ∈ s, m x) (r i * ∏ x ∈ s, r x))
Tactic: rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
have grw : ∀ x ∈ f.support, ∀ y ∈ g.support, degb (x + y) ≤ f.support.sup degb + g.support.sup degb
Tactic: grw [support_mul, Finset.sup_add_le]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.support
_gd : A
gds : _gd ∈ g.support
⊢ degb (_fd + _gd) ≤ f.support.sup degb + g.support.sup degb
have grw : degb _fd + degb _gd ≤ f.support.sup degb + g.support.sup degb
Tactic: grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.support
_gd : A
gds : _gd ∈ g.support
grw : degb _fd + degb _gd ≤ f.support.sup degb + g.support.sup degb
⊢ degb (_fd + _gd) ≤ f.support.sup degb + g.support.sup degb
have grw₁ : degb _fd + degb _gd ≤ degb _fd + g.support.sup degb
Tactic: grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.support
_gd : A
gds : _gd ∈ g.support
grw : degb _fd + degb _gd ≤ f.support.sup degb + g.support.sup degb
grw₁ : degb _fd + degb _gd ≤ degb _fd + g.support.sup degb
⊢ degb (_fd + _gd) ≤ f.support.sup degb + g.support.sup degb
have grw₂ : degb _fd + degb _gd ≤ degb _fd + degb _gd
Tactic: grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
have grw : (f.support + g.support).sup degb ≤ f.support.sup degb + g.support.sup degb
Tactic: classical
  grw [support_mul, Finset.sup_add_le]
  rintro _fd fds _gd gds
  grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
grw : (f.support + g.support).sup degb ≤ f.support.sup degb + g.support.sup degb
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
have grw₁ : ∀ x ∈ f.support, ∀ y ∈ g.support, degb (x + y) ≤ f.support.sup degb + g.support.sup degb
Tactic: classical
  grw [support_mul, Finset.sup_add_le]
  rintro _fd fds _gd gds
  grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ Finset.sup (Finsupp.support.{u_3, u_1} (M := R) (List.prod [])) degb ≤
    List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) [])
have rw : ∀ (b : A), Membership.mem (γ := Finset A) (Finsupp.support.{u_3, u_1} (M := R) 1) b → degb b ≤ 0
Tactic: rw [List.map_nil, Finset.sup_le_iff, List.prod_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f :: fs).prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (f :: fs))
have rw : (f * fs.prod).support.sup degb ≤ f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
Tactic: rw [List.prod_cons, List.map_cons, List.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f * fs.prod).support.sup degb ≤ f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
have grw : f.support.sup degb + fs.prod.support.sup degb ≤
  f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
Tactic: grw [sup_support_mul_le degbm, sup_support_list_prod_le degb0 degbm]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
grw :
  f.support.sup degb + fs.prod.support.sup degb ≤
    f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
⊢ (f * fs.prod).support.sup degb ≤ f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
have grw₁ : f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs) ≤
  f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
Tactic: grw [sup_support_mul_le degbm, sup_support_list_prod_le degb0 degbm]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ List.sum (List.map (fun (f : R[A]) ↦ f.support.inf degt) l) ≤ l.prod.support.inf degt
have refine : LE.le (α := Tᵒᵈ)
  (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
    (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) sorry (Multiset.map degt l.prod.support.val))
  (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))
Tactic: refine OrderDual.ofDual_le_ofDual.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ LE.le (α := Tᵒᵈ)
    (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
      (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val))
    (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))
have refine_1 : degt 0 ≤ 0
Tactic: refine sup_support_list_prod_le ?_ ?_ l