awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
f : α → GradedMonoid A
rw :
  (List.map f l).prod =
    List.prod (List.map (fun (a : α) ↦ Sigma.mk (β := A) ((f a).fst (β := A)) ((f a).snd (β := A))) l)
⊢ (List.map f l).prod =
    mk (A := A) (l.dProdIndex fun (i : α) ↦ (f i).fst (β := A))
      (l.dProd (A := A) (fun (i : α) ↦ (f i).fst (β := A)) fun (i : α) ↦ (f i).snd (β := A))

Tactic:
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]

Premises used: GradedMonoid.mk_list_dProd, GradedMonoid.mk
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod =
    List.prod (List.map (fun (a : α) ↦ Sigma.mk (β := A) ((f a).fst (β := A)) ((f a).snd (β := A))) l)

Tactic:
simp_rw [Sigma.eta]

Premises used: Sigma.eta
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
rw :
  (List.map f (List.finRange n)).prod =
    mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))
rw₁ rw₂ :
  Eq (α := GradedMonoid A)
    (mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A)))
    (mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A)))
⊢ (List.ofFn f).prod =
    mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))

Tactic:
rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]

Premises used: GradedMonoid.list_prod_map_eq_dProd, List.ofFn_eq_map
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
rw : Eq.{u_2 + 1} (α := R) (@GradedMonoid.GOne.one _ (fun (x : ι) ↦ R) AddZero.toZero _ : R) (1 : R)
⊢ dProd (A := fun (x : ι) ↦ R) [] fι fA = (map fA []).prod

Tactic:
rw [List.dProd_nil, List.map_nil, List.prod_nil]

Premises used: List.dProd_nil, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ Eq.{u_2 + 1} (α := R) (@GradedMonoid.GOne.one _ (fun (x : ι) ↦ R) AddZero.toZero _ : R) (1 : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
rw :
  @GradedMonoid.GMul.mul _ (fun (x : ι) ↦ R) AddSemigroup.toAdd _ (fι head) (tail.dProdIndex fι) (fA head)
      (map fA tail).prod =
    fA head * (map fA tail).prod
⊢ (head :: tail).dProd (A := fun (x : ι) ↦ R) fι fA = (map fA (head :: tail)).prod

Tactic:
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]

Premises used: List.map_cons, List.dProd_cons, List.prod_cons
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ @GradedMonoid.GMul.mul _ (fun (x : ι) ↦ R) AddSemigroup.toAdd _ (fι head) (tail.dProdIndex fι) (fA head)
      (map fA tail).prod =
    fA head * (map fA tail).prod

Tactic:
rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ l.dProd (A := fun (x : ι) ↦ R) fι fA = (map fA l).prod

Tactic:
match l with
  | [] =>
    rw [List.dProd_nil, List.map_nil, List.prod_nil]
    rfl
  | head::tail =>
    rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
    rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : One R
inst_2 : Zero ι
A : ι → S
inst_3 : GradedOne A
⊢ 1 ∈ A 0

Tactic:
SetLike.GradedOne.one_mem

Premises used: SetLike.GradedOne.one_mem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : One R
inst_2 : Zero ι
A : ι → S
inst_3 : GradedOne A
⊢ Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) inst_2 _ : ↥(A 0)) : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Mul R
inst_2 : Add ι
A : ι → S
inst_3 : GradedMul A
i j : ι
gi gj : R
hi : gi ∈ A i
hj : gj ∈ A j
⊢ gi * gj ∈ A (i + j)

Tactic:
SetLike.GradedMul.mul_mem hi hj

Premises used: SetLike.GradedMul.mul_mem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Mul R
inst_2 : Add ι
A : ι → S
inst_3 : GradedMul A
i j : ι
x : ↥(A i)
y : ↥(A j)
⊢ (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) inst_2 _ _ _ x y : ↥(A (i + j))) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
⊢ Eq.{u_2 + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
a b : ↥(A 0)
⊢ (↑(a * b) : R) = (↑a : R) * (↑b : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
a : ↥(A 0)
n : ℕ
⊢ (↑(a ^ n) : R) = (↑a : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
rw : 1 ∈ A 0
⊢ HPow.hPow (β := ℕ) r 0 ∈ A (HSMul.hSMul (α := ℕ) 0 i)

Tactic:
rw [pow_zero, zero_nsmul]

Premises used: pow_zero, zero_nsmul
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0

Tactic:
one_mem_graded _

Premises used: SetLike.one_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Premises used: SetLike.one_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n_1 : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
rw : r * r ^ n ∈ A (i + n • i)
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)

Tactic:
rw [pow_succ', succ_nsmul']

Premises used: succ_nsmul', pow_succ'
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n_1 : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)

Tactic:
mul_mem_graded h (pow_mem_graded n h)

Premises used: SetLike.mul_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n_1 : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)

Tactic:
exact mul_mem_graded h (pow_mem_graded n h)

Premises used: SetLike.mul_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)

Tactic:
match n with
  | 0 =>
    rw [pow_zero, zero_nsmul]
    exact one_mem_graded _
  | n + 1 =>
    rw [pow_succ', succ_nsmul']
    exact mul_mem_graded h (pow_mem_graded n h)
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), Membership.mem (γ := List ι') [] j → r j ∈ A (i j)
rw : 1 ∈ A 0
⊢ (List.map r []).prod ∈ A (List.map i []).sum

Tactic:
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]

Premises used: List.sum_nil, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), Membership.mem (γ := List ι') [] j → r j ∈ A (i j)
⊢ 1 ∈ A 0

Tactic:
one_mem_graded _

Premises used: SetLike.one_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), Membership.mem (γ := List ι') [] j → r j ∈ A (i j)
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Premises used: SetLike.one_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
rw : r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)
⊢ (List.map r (head :: tail)).prod ∈ A (List.map i (head :: tail)).sum

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]

Premises used: List.map_cons, List.sum_cons, List.prod_cons
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)

Tactic:
mul_mem_graded (h _ List.mem_cons_self)
        (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)

Premises used: List.mem_cons_of_mem, SetLike.mul_mem_graded, List.mem_cons_self
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)

Tactic:
exact
      mul_mem_graded (h _ List.mem_cons_self)
        (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)

Premises used: List.mem_cons_of_mem, SetLike.mul_mem_graded, List.mem_cons_self
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ l, r j ∈ A (i j)
⊢ (List.map r l).prod ∈ A (List.map i l).sum

Tactic:
match l with
  | [] =>
    rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
    exact one_mem_graded _
  | head::tail =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
    exact
      mul_mem_graded (h _ List.mem_cons_self)
        (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
rw : (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
⊢ (List.ofFn r).prod ∈ A (List.ofFn i).sum

Tactic:
rw [List.ofFn_eq_map, List.ofFn_eq_map]

Premises used: List.ofFn_eq_map
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum

Tactic:
list_prod_map_mem_graded _ _ _ fun _ _ => h _

Premises used: SetLike.list_prod_map_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum

Tactic:
exact list_prod_map_mem_graded _ _ _ fun _ _ => h _

Premises used: SetLike.list_prod_map_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
i : ι
x : ↥(A i)
n : ℕ
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(A i)) inst_2 _ n _ x : ↥(A (n • i))) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
rw :
  Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) AddZero.toZero _ : ↥(A 0)) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
rw₁ : Eq.{u_2 + 1} (α := R) 1 (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
rw₂ : Eq.{u_2 + 1} (α := R) 1 (List.prod [])
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Eq.{u_2 + 1} (α := R) (↑(List.dProd (A := fun (i : ι) ↦ ↥(A i)) [] fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))

Tactic:
rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]

Premises used: SetLike.coe_gOne, List.dProd_nil, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
rw :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
            (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
          ↥(A (fι head + tail.dProdIndex fι))) :
      R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₁ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₂ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    ((↑(fA head) : R) :: List.map (fun (a : α) ↦ (↑(fA a) : R)) tail).prod
rw₃ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail)
rw₄ rw₅ :
  (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail) =
    (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail)
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))

Tactic:
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]

Premises used: List.map_cons, SetLike.coe_gMul, List.dProd_cons, List.prod_cons
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ Eq.{u_2 + 1} (α := R) (↑(l.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) l))

Tactic:
match l with
  | [] =>
    rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
  | head::tail =>
    rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ Eq.{u_2 + 1} (α := ↥(A (l.dProdIndex fι))) (l.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (l.dProdIndex fι)))
    (Subtype.mk (p := fun (x : R) ↦ x ∈ A (l.dProdIndex fι)) (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) l)) ⋯ :
      ↥(A (l.dProdIndex fι)))

Tactic:
Subtype.ext <| SetLike.coe_list_dProd _ _ _ _

Premises used: SetLike.coe_list_dProd, Subtype.ext
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
A : ι → S
i : ι
x : ↥(A i)
⊢ IsHomogeneousElem A (↑x : R)

Tactic:
⟨i, x.prop⟩

Premises used: Subtype.prop, Exists.intro, SetLike.IsHomogeneousElem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Zero ι
inst_2 : One R
A : ι → S
inst_3 : GradedOne A
⊢ IsHomogeneousElem A 1

Tactic:
⟨0, SetLike.one_mem_graded _⟩

Premises used: SetLike.one_mem_graded, Exists.intro, OfNat.ofNat, SetLike.IsHomogeneousElem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
insert :
  ∀ (a : κ) (s : Finset κ),
    a ∉ s →
      (∀ (hF : ∀ k ∈ s, g k ∈ A (i k)), ∏ k ∈ s, g k ∈ A (∑ k ∈ s, i k)) →
        ∀ (hF : ∀ k ∈ Insert.insert a s, g k ∈ A (i k)), ∏ k ∈ Insert.insert a s, g k ∈ A (∑ k ∈ Insert.insert a s, i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)

Tactic:
induction F using Finset.induction_on
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)
⊢ ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)

Tactic:
simp [GradedOne.one_mem]

Premises used: SetLike.GradedOne.one_mem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
rw : g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)
⊢ ∏ k ∈ insert j F', g k ∈ A (∑ k ∈ insert j F', i k)

Tactic:
rw [Finset.prod_insert hF2, Finset.sum_insert hF2]

Premises used: Finset.prod_insert, Finset.sum_insert
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j ∈ A (i j)

Tactic:
grind
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
apply : ∏ x ∈ F', g x ∈ A (∑ x ∈ F', i x)
⊢ g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)

Tactic:
apply SetLike.mul_mem_graded (by grind)

Premises used: SetLike.mul_mem_graded
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ x ∈ F', g x ∈ A (∑ x ∈ F', i x)

Tactic:
grind
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
insert insert₁ :
  ∀ (a : κ) (s : Finset κ),
    a ∉ s →
      (∀ (hF : ∀ k ∈ s, g k ∈ A (i k)), ∏ k ∈ s, g k ∈ A (∑ k ∈ s, i k)) →
        ∀ (hF : ∀ k ∈ Insert.insert a s, g k ∈ A (i k)), ∏ k ∈ Insert.insert a s, g k ∈ A (∑ k ∈ Insert.insert a s, i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)

Tactic:
classical
  induction F using Finset.induction_on
  · simp [GradedOne.one_mem]
  · case insert j F' hF2 h3 =>
    rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
    apply SetLike.mul_mem_graded (by grind)
    grind

Premises used: SetLike.mul_mem_graded, Insert.insert, SetLike.GradedOne.one_mem
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
n : κ → ℕ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ^ n k ∈ A (∑ k ∈ F, n k • i k)

Tactic:
prod_mem_graded A _ _ fun k hk ↦ pow_mem_graded _ (hF k hk)

Premises used: SetLike.prod_mem_graded, SetLike.pow_mem_graded
-- Module: Mathlib.Algebra.GradedMulAction
Goal:
ιA : Type u_1
ιM : Type u_3
A : ιA → Type u_4
M : ιM → Type u_5
inst : VAdd ιA ιM
inst_1 : GSMul A M
i : ιA
j : ιM
a : A i
b : M j
⊢ mk (A := A) i a • mk (A := M) j b = mk (A := M) (i +ᵥ j) (GSMul.smul (A := A) (M := M) a b)

Tactic:
rfl

Premises used: rfl, GradedMonoid.mk
-- Module: Mathlib.Algebra.GradedMulAction
Goal:
ιA : Type u_1
ιB : Type u_2
S : Type u_5
R : Type u_6
N : Type u_7
M : Type u_8
inst : SetLike S R
inst_1 : SetLike N M
inst_2 : SMul R M
inst_3 : VAdd ιA ιB
A : ιA → S
B : ιB → N
inst_4 : GradedSMul A B
i : ιA
j : ιB
x : ↥(A i)
y : ↥(B j)
⊢ (↑(@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(A i)) (fun (i : ιB) ↦ ↥(B i)) inst_3 _ _ _ x y : ↥(B (i +ᵥ j))) :
      M) =
    (↑x : R) • (↑y : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
inst_2 : FaithfulSMul α β
⊢ Function.Injective.{u_5 + 1, u_6 + 1} (α := α) (β := Equiv.Perm β) toPerm

Tactic:
(show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp

Premises used: smul_left_injective', Function.Injective.of_comp
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
⊢ Function.Bijective (β := β) fun (x : β) ↦ g • x

Tactic:
(MulAction.toPerm g).bijective

Premises used: Equiv.bijective, MulAction.toPerm
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
⊢ Function.Injective (β := β) fun (x : β) ↦ g • x

Tactic:
(MulAction.bijective g).injective

Premises used: MulAction.bijective, Function.Bijective.injective