awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
v : (i : Fin n) → M
⊢ (((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
              (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
            (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
              (MultilinearMap.mkPiRing R (Fin n) 1)
              (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))) :
          (⨂[R] (i : Fin n), M) →ₗ[R] R) :
        (a : ⨂[R] (i : Fin n), M) → R)
      ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) =
    HMul.hMul (β := R) a
      ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                  (MultilinearMap.mkPiRing R (Fin n) 1)
                  (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
              (⨂[R] (i : Fin n), M) →ₗ[R] R) :
            (a : ⨂[R] (i : Fin n), M) → R)
          ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
        R)
have H : HSMul.hSMul (β := R) a
    ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R)
        (Function.update (β := fun (x : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i))) :
      R) =
  HMul.hMul (β := R) a
    ((MultilinearMap.mkPiRing R (Fin n) 1 : (a : (i : Fin n) → R) → R) fun (i_1 : Fin n) ↦
        Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) i_1 :
      R)
Tactic: simp only [lift.tprod, MultilinearMap.compLinearMap_apply, this,
         LinearMap.smul_apply, MultilinearMap.map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
⊢ (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)))
have of : 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: apply isEmpty_or_nonempty ι |>.elim
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
of :
  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)))
⊢ (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)))
have of₁ : Nonempty ι →
  (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: apply isEmpty_or_nonempty ι |>.elim
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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 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)))
have 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
Tactic: convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
⊢ (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)))
have 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)
Tactic: convert!
          AddConGen.Rel.of _ _ <|
            SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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 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
have 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)
Tactic: rw [MultilinearMap.map_update_smul, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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)
⊢ 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
have 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)
Tactic: rw [MultilinearMap.map_update_smul, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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)) =
    (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)
have 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)
Tactic: simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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 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)))
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
⊢ (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)))
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have 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)))
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
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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 + y_1)) (r • (x_1 + z))
have add : (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • w + r • y_1) (r • x_1 + r • z)
Tactic: rw [smul_add, smul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have refl : ∀ (x : ⨂[R] (x : ι), M), (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • x)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Symmetric (goal)
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)
⊢ (addConGen (Rel R ι M) : (a : ⨂[R] (x : ι), M) → (⨂[R] (x : ι), M) → Prop) (r • x) (r • y)
have 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)
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
Cleared hypotheses: h