awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : IsEmpty ι
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))

Tactic:
addConGen (Rel R ι M) |>.refl _

Premises used: addConGen, SymmetricPower.Rel, AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : IsEmpty ι
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)))

Tactic:
convert! addConGen (Rel R ι M) |>.refl _

Premises used: addConGen, SymmetricPower.Rel, AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ AddConGen.Rel (M := ⨂[R] (i : ι), M) (Rel R ι M)
    ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) i_1)
    ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) ((e : (a : ι) → ι) i_1))

Tactic:
AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)

Premises used: Function.update, SymmetricPower.Rel.perm, AddConGen.Rel.of, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
h₁ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) i_1
h₂ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) ((e : (a : ι) → ι) i_1)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)))

Tactic:
convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)

Premises used: Function.update, SymmetricPower.Rel.perm, AddConGen.Rel.of, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
h₁ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i) =
    HSMul.hSMul (β := ⨂[R] (i : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M)
          (Function.update (β := fun (x : ι) ↦ M) f i (f i)) :
        ⨂[R] (i : ι), M)
h₂ h₃ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i) =
    HSMul.hSMul (β := ⨂[R] (i : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) f : ⨂[R] (i : ι), M)
⊢ HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) i_1

Tactic:
rw [MultilinearMap.map_update_smul, Function.update_eq_self]

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
h₁ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) (f ∘ (⇑e : (a : ι) → ι)) :
        ⨂[R] (i : ι), M)
⊢ HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) ((e : (a : ι) → ι) i_1)

Tactic:
simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, Function.update_comp_equiv, Function.update_apply_equiv_apply
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
⊢ HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) (f ∘ (⇑e : (a : ι) → ι)) :
        ⨂[R] (i : ι), M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
h : Nonempty ι
i : ι := h.some
h₁ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) i_1
h₂ h₃ :
  HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)) =
    (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i_1 : ι) ↦
      Function.update (β := fun (a : ι) ↦ M) f i (r • f i) ((e : (a : ι) → ι) i_1)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
    (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
      ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
        f ((e : (a : ι) → ι) i)))

Tactic:
classical
        convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, Function.update_comp_equiv, SymmetricPower.Rel.perm, AddConGen.Rel.of, Function.update_apply_equiv_apply
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x_1 y_1 x y : ⨂[R] (x : ι), M
h : Rel R ι M x y
of :
  ∀ (e : Perm ι) (f : ι → M),
    (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop)
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ f i))
      (HSMul.hSMul (β := ⨂[R] (x : ι), M) r
        ((PiTensorProduct.tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦
          f ((e : (a : ι) → ι) i)))
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)

Tactic:
cases h with
    | perm e f =>
      apply isEmpty_or_nonempty ι |>.elim <;> intro h
      · convert! addConGen (Rel R ι M) |>.refl _
      · let i := Nonempty.some h
        classical
        convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, addConGen, SymmetricPower.Rel, Function.update_comp_equiv, isEmpty_or_nonempty, AddConGen.Rel.of, Or.elim, Function.update_apply_equiv_apply, AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 : ⨂[R] (x : ι), M
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • x_1)

Tactic:
AddCon.refl _ _

Premises used: AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 : ⨂[R] (x : ι), M
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • x_1)

Tactic:
exact AddCon.refl _ _

Premises used: AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 y_1 : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) x_1 y_1
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
symm : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • x_1)

Tactic:
apply AddCon.symm

Premises used: AddCon.symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 y_1 : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) x_1 y_1
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) x_1 y_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
trans : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
trans₁ : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
trans₂ : ⨂[R] (x : ι), M
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • z)

Tactic:
apply AddCon.trans

Premises used: AddCon.trans
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) x_1 y_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) x_1 y_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x_1) (r • y_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y w x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) w x_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
add : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w + r • y_1) (r • x_1 + r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • (w + y_1)) (r • (x_1 + z))

Tactic:
rw [smul_add, smul_add]

Premises used: smul_add
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y w x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) w x_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
add : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)
add₁ : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w + r • y_1) (r • x_1 + r • z)

Tactic:
apply AddCon.add

Premises used: AddCon.add
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y w x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) w x_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y w x_1 y_1 z : ⨂[R] (x : ι), M
h : AddConGen.Rel (Rel R ι M) w x_1
h_1 : AddConGen.Rel (Rel R ι M) y_1 z
a_ih : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x_1)
a_ih_1 : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y_1) (r • z)

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x y : ⨂[R] (x : ι), M
h : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) x y
of :
  ∀ (x y : ⨂[R] (x : ι), M) (h : Rel R ι M x y),
    (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
refl :
  ∀ (x : ⨂[R] (x : ι), M), (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • x)
symm :
  ∀ {x y : ⨂[R] (x : ι), M},
    AddConGen.Rel (Rel R ι M) x y →
      (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y) →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • x)
trans :
  ∀ {x y z : ⨂[R] (x : ι), M},
    AddConGen.Rel (Rel R ι M) x y →
      AddConGen.Rel (Rel R ι M) y z →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y) →
          (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • z) →
            (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • z)
add :
  ∀ {w x y z : ⨂[R] (x : ι), M},
    AddConGen.Rel (Rel R ι M) w x →
      AddConGen.Rel (Rel R ι M) y z →
        (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w) (r • x) →
          (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • y) (r • z) →
            (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • (w + y)) (r • (x + z))
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)

Tactic:
induction h with
  | of x y h => cases h with
    | perm e f =>
      apply isEmpty_or_nonempty ι |>.elim <;> intro h
      · convert! addConGen (Rel R ι M) |>.refl _
      · let i := Nonempty.some h
        classical
        convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl
  | refl => exact AddCon.refl _ _
  | symm => apply AddCon.symm; assumption
  | trans => apply AddCon.trans <;> assumption
  | add => rw [smul_add, smul_add]; apply AddCon.add <;> assumption

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, addConGen, AddCon.add, SymmetricPower.Rel, Function.update_comp_equiv, isEmpty_or_nonempty, AddConGen.Rel.of, AddCon.trans, AddCon.symm, symm, Or.elim, refl, Function.update_apply_equiv_apply, smul_add, AddCon.refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Perm ι
f : ι → M
⊢ Eq (α := Sym[R] ι M) (⨂ₛ[R] (i : ι), f ((e : (a : ι) → ι) i)) (⨂ₛ[R] (i : ι), f i)

Tactic:
Eq.symm <| Quot.sound <| AddConGen.Rel.of _ _ <| Rel.perm e f

Premises used: Quot.sound, SymmetricPower.Rel.perm, AddConGen.Rel.of, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Perm ι
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ M) Sym[R] ι M) (MultilinearMap.domDomCongr e (tprod R)) (tprod R)

Tactic:
MultilinearMap.ext <| tprod_equiv e

Premises used: MultilinearMap.ext, SymmetricPower.tprod_equiv
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R Sym[R] ι M) (LinearMap.range (mk R ι M)) ⊤

Tactic:
LinearMap.range_eq_top_of_surjective _ AddCon.mk'_surjective

Premises used: LinearMap.range_eq_top_of_surjective, AddCon.mk'_surjective
-- Module: Mathlib.LinearAlgebra.TensorPower.Symmetric
Goal:
R ι : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (⇑(LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (mk R ι M)
              (PiTensorProduct.tprod R (s := fun (x : ι) ↦ M))) :
          (a : (i : ι) → M) → Sym[R] ι M)))
    ⊤
rw₁ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.range (ι := (i : ι) → M)
        (Function.comp (β := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₂ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R
      (Set.image (α := ⨂[R] (x : ι), M) (⇑(mk R ι M) : (a : ⨂[R] (x : ι), M) → Sym[R] ι M)
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₃ :
  Eq (α := Submodule R Sym[R] ι M)
    (Submodule.map (mk R ι M)
      (Submodule.span R
        (Set.range (ι := (i : ι) → M)
          (⇑(PiTensorProduct.tprod R (s := fun (x : ι) ↦ M)) : (a : (i : ι) → M) → ⨂[R] (x : ι), M))))
    ⊤
rw₄ : Eq (α := Submodule R Sym[R] ι M) (Submodule.map (mk R ι M) ⊤) ⊤
rw₅ : Eq (α := Submodule R Sym[R] ι M) (LinearMap.range (mk R ι M)) ⊤
rw₆ rw₇ : Eq (α := Submodule R Sym[R] ι M) ⊤ ⊤
⊢ Eq (α := Submodule R Sym[R] ι M)
    (Submodule.span R (Set.range (ι := (i : ι) → M) (⇑(tprod R) : (a : (i : ι) → M) → Sym[R] ι M))) ⊤

Tactic:
rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]

Premises used: Set.range_comp, SymmetricPower.tprod, Submodule.map_top, LinearMap.coe_compMultilinearMap, SymmetricPower.range_mk, PiTensorProduct.span_tprod_eq_top, Submodule.span_image
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
x : M
⊢ Eq (α := M) ((lift (LinearMap.lsmul R M) ∘ₗ (mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1 : (a : M) → M) x : M)
    ((LinearMap.id : (a : M) → M) x : M)

Tactic:
simp