[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = r₁ • 0 + op r₂ • 0
[PROOFSTEP]
rw [smul_zero, zero_add, smul_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 • m₂ + 0 • m₁ = 0
[PROOFSTEP]
rw [zero_smul, zero_add, zero_smul]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ r • m + 0 • 0 = r • m
[PROOFSTEP]
rw [smul_zero, add_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ 0 • 0 + op r • m = op r • m
[PROOFSTEP]
rw [smul_zero, zero_add]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
src✝¹ : One (tsze R M) := one
src✝ : Mul (tsze R M) := mul
x : tsze R M
⊢ 1 • x.snd + op x.fst • 0 = x.snd
[PROOFSTEP]
rw [one_smul, smul_zero, add_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
src✝¹ : One (tsze R M) := one
src✝ : Mul (tsze R M) := mul
x : tsze R M
⊢ x.fst • 0 + 1 • x.snd = x.snd
[PROOFSTEP]
rw [smul_zero, zero_add, one_smul]
[GOAL]
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
ext
[GOAL]
case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ fst (NatCast.natCast (x✝ + 1)) = fst (NatCast.natCast x✝ + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ snd (NatCast.natCast (x✝ + 1)) = snd (NatCast.natCast x✝ + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x₁ x₂ x₃ : tsze R M
⊢ x₁.fst • (x₂.snd + x₃.snd) + (op x₂.fst + op x₃.fst) • x₁.snd =
    x₁.fst • x₂.snd + op x₂.fst • x₁.snd + (x₁.fst • x₃.snd + op x₃.fst • x₁.snd)
[PROOFSTEP]
simp_rw [smul_add, add_smul, add_add_add_comm]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x₁ x₂ x₃ : tsze R M
⊢ (x₁.fst + x₂.fst) • x₃.snd + op x₃.fst • (x₁.snd + x₂.snd) =
    x₁.fst • x₃.snd + op x₃.fst • x₁.snd + (x₂.fst • x₃.snd + op x₃.fst • x₂.snd)
[PROOFSTEP]
simp_rw [add_smul, smul_add, add_add_add_comm]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x : tsze R M
⊢ 0 • x.snd + op x.fst • 0 = 0
[PROOFSTEP]
rw [zero_smul, zero_add, smul_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x : tsze R M
⊢ x.fst • 0 + 0 • x.snd = 0
[PROOFSTEP]
rw [smul_zero, zero_add, zero_smul]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ snd (x ^ n) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
have : ∀ n : ℕ, op (x.fst ^ n) • x.snd = x.fst ^ n • x.snd :=
  by
  intro n
  induction' n with n ih
  · simp
  · rw [pow_succ', MulOpposite.op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
[PROOFSTEP]
intro n
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
n : ℕ
⊢ op (fst x ^ n) • snd x = fst x ^ n • snd x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ op (fst x ^ Nat.zero) • snd x = fst x ^ Nat.zero • snd x
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
n : ℕ
ih : op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ op (fst x ^ Nat.succ n) • snd x = fst x ^ Nat.succ n • snd x
[PROOFSTEP]
rw [pow_succ', MulOpposite.op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ snd (x ^ n) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
simp_rw [snd_pow_eq_sum, this, smul_smul, ← pow_add]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred n - i + i) • snd x) (List.range n)) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
match n with
| 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
| (Nat.succ n) =>
  simp_rw [Nat.pred_succ]
  refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _
  · rintro m hm
    simp_rw [List.mem_map, List.mem_range] at hm 
    obtain ⟨i, hi, rfl⟩ := hm
    rw [tsub_add_cancel_of_le (Nat.lt_succ_iff.mp hi)]
  · rw [List.length_map, List.length_range]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred 0 - i + i) • snd x) (List.range 0)) = 0 • fst x ^ Nat.pred 0 • snd x
[PROOFSTEP]
rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred (Nat.succ n) - i + i) • snd x) (List.range (Nat.succ n))) =
    Nat.succ n • fst x ^ Nat.pred (Nat.succ n) • snd x
[PROOFSTEP]
simp_rw [Nat.pred_succ]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))) = Nat.succ n • fst x ^ n • snd x
[PROOFSTEP]
refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ ∀ (x_1 : M), x_1 ∈ List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n)) → x_1 = fst x ^ n • snd x
[PROOFSTEP]
rintro m hm
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
m : M
hm : m ∈ List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))
⊢ m = fst x ^ n • snd x
[PROOFSTEP]
simp_rw [List.mem_map, List.mem_range] at hm 
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
m : M
hm : ∃ a, a < Nat.succ n ∧ fst x ^ (n - a + a) • snd x = m
⊢ m = fst x ^ n • snd x
[PROOFSTEP]
obtain ⟨i, hi, rfl⟩ := hm
[GOAL]
case refine'_1.intro.intro
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n i : ℕ
hi : i < Nat.succ n
⊢ fst x ^ (n - i + i) • snd x = fst x ^ n • snd x
[PROOFSTEP]
rw [tsub_add_cancel_of_le (Nat.lt_succ_iff.mp hi)]
[GOAL]
case refine'_2
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.length (List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))) • fst x ^ n • snd x =
    Nat.succ n • fst x ^ n • snd x
[PROOFSTEP]
rw [List.length_map, List.length_range]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
n : ℕ
⊢ snd (inl r ^ n) = snd (inl (r ^ n))
[PROOFSTEP]
simp [snd_pow_eq_sum]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x y z : tsze R M
⊢ (x.fst * y.fst) • z.snd + op z.fst • (x.fst • y.snd + op y.fst • x.snd) =
    x.fst • (y.fst • z.snd + op z.fst • y.snd) + (op z.fst * op y.fst) • x.snd
[PROOFSTEP]
simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
⊢ snd ((fun n x => x ^ n) 0 x) = snd 1
[PROOFSTEP]
simp [snd_pow_eq_sum]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
n : ℕ
x : tsze R M
⊢ snd ((fun n x => x ^ n) (n + 1) x) = snd (x * (fun n x => x ^ n) n x)
[PROOFSTEP]
simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
n : ℕ
x : tsze R M
⊢ List.sum (List.map (fun i => fst x ^ (n - i) • op (fst x ^ i) • snd x) (List.range (n + 1))) =
    fst x • List.sum (List.map (fun i => fst x ^ (Nat.pred n - i) • op (fst x ^ i) • snd x) (List.range n)) +
      op (fst (x ^ n)) • snd x
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
⊢ List.sum (List.map (fun i => fst x ^ (Nat.zero - i) • op (fst x ^ i) • snd x) (List.range (Nat.zero + 1))) =
    fst x •
        List.sum (List.map (fun i => fst x ^ (Nat.pred Nat.zero - i) • op (fst x ^ i) • snd x) (List.range Nat.zero)) +
      op (fst (x ^ Nat.zero)) • snd x
[PROOFSTEP]
simp [List.range_succ]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝ + 1))) =
    fst x •
        List.sum
          (List.map (fun i => fst x ^ (Nat.pred (Nat.succ n✝) - i) • op (fst x ^ i) • snd x)
            (List.range (Nat.succ n✝))) +
      op (fst (x ^ Nat.succ n✝)) • snd x
[PROOFSTEP]
simp_rw [Nat.pred_succ]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝ + 1))) =
    fst x • List.sum (List.map (fun i => fst x ^ (n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝))) +
      op (fst (x ^ Nat.succ n✝)) • snd x
[PROOFSTEP]
rw [List.range_succ, List.map_append, List.sum_append, List.map_singleton, List.sum_singleton, Nat.sub_self, pow_zero,
  one_smul, List.smul_sum, List.map_map, fst_pow]
  --porting note: `Function.comp` no longer works in `rw` so move to `simp_rw`
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x =
    List.sum
        (List.map ((fun x x_1 => x • x_1) (fst x) ∘ fun i => fst x ^ (n✝ - i) • op (fst x ^ i) • snd x)
          (List.range (Nat.succ n✝))) +
      op (fst x ^ Nat.succ n✝) • snd x
[PROOFSTEP]
simp_rw [Function.comp, smul_smul, ← pow_succ, Nat.succ_eq_add_one]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x =
    List.sum (List.map (fun x_1 => fst x ^ (n✝ - x_1 + 1) • op (fst x ^ x_1) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x
[PROOFSTEP]
congr 2
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.map (fun i => fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1)) =
    List.map (fun x_1 => fst x ^ (n✝ - x_1 + 1) • op (fst x ^ x_1) • snd x) (List.range (n✝ + 1))
[PROOFSTEP]
refine' List.map_congr fun i hi => _
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ i : ℕ
hi : i ∈ List.range (n✝ + 1)
⊢ fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x = fst x ^ (n✝ - i + 1) • op (fst x ^ i) • snd x
[PROOFSTEP]
rw [List.mem_range, Nat.lt_succ_iff] at hi 
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ i : ℕ
hi : i ≤ n✝
⊢ fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x = fst x ^ (n✝ - i + 1) • op (fst x ^ i) • snd x
[PROOFSTEP]
rw [Nat.sub_add_comm hi]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ snd (List.prod l) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst l)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst l))) • snd x.snd)
        (List.enum l))
[PROOFSTEP]
induction' l with x xs ih
[GOAL]
case nil
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
⊢ snd (List.prod []) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst [])) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst []))) • snd x.snd)
        (List.enum []))
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ snd (List.prod (x :: xs)) =
    List.sum
      (List.map
        (fun x_1 =>
          List.prod (List.take x_1.fst (List.map fst (x :: xs))) •
            op (List.prod (List.drop (Nat.succ x_1.fst) (List.map fst (x :: xs)))) • snd x_1.snd)
        (List.enum (x :: xs)))
[PROOFSTEP]
rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom]
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ snd (List.prod (x :: xs)) =
    List.sum
      (List.map
        (fun x_1 =>
          List.prod (List.take x_1.fst (List.map fst (x :: xs))) •
            op (List.prod (List.drop (Nat.succ x_1.fst) (List.map fst (x :: xs)))) • snd x_1.snd)
        ((0, x) :: List.map (Prod.map (fun x => x + 1) id) (List.enum xs)))
[PROOFSTEP]
simp_rw [List.map_cons, List.map_map, Function.comp, Prod.map_snd, Prod.map_fst, id, List.take_zero, List.take_cons,
  List.prod_nil, List.prod_cons, snd_mul, one_smul, List.drop, mul_smul, List.sum_cons, fst_list_prod, ih,
  List.smul_sum, List.map_map]
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ List.sum
        (List.map
          ((fun x_1 => fst x • x_1) ∘ fun x =>
            List.prod (List.take x.fst (List.map fst xs)) •
              op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
          (List.enum xs)) +
      op (List.prod (List.map fst xs)) • snd x =
    op (List.prod (List.map fst xs)) • snd x +
      List.sum
        (List.map
          (fun x_1 =>
            fst x •
              List.prod (List.take x_1.fst (List.map fst xs)) •
                op (List.prod (List.drop (x_1.fst + 1) (List.map fst xs))) • snd x_1.snd)
          (List.enum xs))
[PROOFSTEP]
exact add_comm _ _
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommMonoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
src✝ : Monoid (tsze R M) := monoid
x₁ x₂ : tsze R M
⊢ x₁.fst • x₂.snd + op x₂.fst • x₁.snd = x₂.fst • x₁.snd + op x₁.fst • x₂.snd
[PROOFSTEP]
rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
s : S
x : (fun x => tsze R M) s
⊢ ↑(algebraMap S R) s • snd x + op (fst x) • 0 = fst x • 0 + op (↑(algebraMap S R) s) • snd x
[PROOFSTEP]
rw [smul_zero, smul_zero, add_zero, zero_add]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
s : S
x : (fun x => tsze R M) s
⊢ ↑(algebraMap S R) s • snd x = op (↑(algebraMap S R) s) • snd x
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, MulOpposite.op_one, smul_assoc, one_smul, smul_assoc, one_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
r : S
x : (fun x => tsze R M) r
⊢ r • x.snd = ↑(algebraMap S R) r • x.snd + op x.fst • 0
[PROOFSTEP]
rw [smul_zero, add_zero, algebraMap_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
⊢ ↑(algebraMap R' A) 1 + ↑f 0 = 1
[PROOFSTEP]
rw [map_zero, map_one, add_zero]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
      ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
        (inl r₁ + inr m₁) *
      ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
        (inl r₂ + inr m₂)
[PROOFSTEP]
dsimp
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(algebraMap R' A) ((r₁ + 0) * (r₂ + 0)) + ↑f ((r₁ + 0) • (0 + m₂) + (op r₂ + 0) • (0 + m₁)) =
    (↑(algebraMap R' A) (r₁ + 0) + ↑f (0 + m₁)) * (↑(algebraMap R' A) (r₂ + 0) + ↑f (0 + m₂))
[PROOFSTEP]
simp only [add_zero, zero_add, add_mul, mul_add, smul_mul_smul, hf, smul_zero, op_smul_eq_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(algebraMap R' A) (r₁ * r₂) + ↑f (r₁ • m₂ + r₂ • m₁) =
    ↑(algebraMap R' A) r₁ * ↑(algebraMap R' A) r₂ + ↑f m₁ * ↑(algebraMap R' A) r₂ + ↑(algebraMap R' A) r₁ * ↑f m₂
[PROOFSTEP]
rw [← RingHom.map_mul, LinearMap.map_add, ← Algebra.commutes _ (f _), ← Algebra.smul_def, ← Algebra.smul_def,
  add_right_comm, add_assoc, LinearMap.map_smul, LinearMap.map_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
m : M
⊢ ↑(algebraMap R' A) 0 + ↑f m = ↑f m
[PROOFSTEP]
rw [RingHom.map_zero, zero_add]
