case refine'_1
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {r_1 : R} {f : (i : ι) → s i}, ↑(liftAux φ) (r • tprodCoeff R r_1 f) = r • ↑(liftAux φ) (tprodCoeff R r_1 f)

case refine'_2
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {x y : ⨂[R] (i : ι), s i},
    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x →
      ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y → ↑(liftAux φ) (r • (x + y)) = r • ↑(liftAux φ) (x + y)
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x
refine' PiTensorProduct.induction_on' x _ _
case refine'_1
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ ↑(liftAux φ) (r • tprodCoeff R z f) = r • ↑(liftAux φ) (tprodCoeff R z f)
case refine'_1
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {r_1 : R} {f : (i : ι) → s i}, ↑(liftAux φ) (r • tprodCoeff R r_1 f) = r • ↑(liftAux φ) (tprodCoeff R r_1 f)
intro z f
no goals
case refine'_1
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ ↑(liftAux φ) (r • tprodCoeff R z f) = r • ↑(liftAux φ) (tprodCoeff R z f)
rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
case refine'_2
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : ↑(liftAux φ) (r • z) = r • ↑(liftAux φ) z
ihy : ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y
⊢ ↑(liftAux φ) (r • (z + y)) = r • ↑(liftAux φ) (z + y)
case refine'_2
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {x y : ⨂[R] (i : ι), s i},
    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x →
      ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y → ↑(liftAux φ) (r • (x + y)) = r • ↑(liftAux φ) (x + y)
intro z y ihz ihy
no goals
case refine'_2
ι : Type u_4
ι₂ : Type ?u.286625
ι₃ : Type ?u.286628
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.286637
R₂ : Type ?u.286640
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.286830
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_3
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.287098
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : ↑(liftAux φ) (r • z) = r • ↑(liftAux φ) z
ihy : ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y
⊢ ↑(liftAux φ) (r • (z + y)) = r • ↑(liftAux φ) (z + y)
rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]