R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.79966
inst✝¹³ : Monoid R'
R'' : Type ?u.79972
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.79984
Q : Type ?u.79987
S : Type ?u.79990
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
C : M ⊗[R] N → Prop
z : M ⊗[R] N
C0 : C 0
C1 : ∀ (x : M) (y : N), C (x ⊗ₜ[R] y)
Cp : ∀ (x y : M ⊗[R] N), C x → C y → C (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : C ↑y
m : M
n : N
⊢ C (↑(FreeAddMonoid.of (m, n)) + ↑y)
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.79966
inst✝¹³ : Monoid R'
R'' : Type ?u.79972
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.79984
Q : Type ?u.79987
S : Type ?u.79990
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
C : M ⊗[R] N → Prop
z : M ⊗[R] N
C0 : C 0
C1 : ∀ (x : M) (y : N), C (x ⊗ₜ[R] y)
Cp : ∀ (x y : M ⊗[R] N), C x → C y → C (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : C ↑y
m : M
n : N
⊢ C ↑(FreeAddMonoid.of (m, n) + y)
rw [AddCon.coe_add]
no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.79966
inst✝¹³ : Monoid R'
R'' : Type ?u.79972
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.79984
Q : Type ?u.79987
S : Type ?u.79990
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
C : M ⊗[R] N → Prop
z : M ⊗[R] N
C0 : C 0
C1 : ∀ (x : M) (y : N), C (x ⊗ₜ[R] y)
Cp : ∀ (x y : M ⊗[R] N), C x → C y → C (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : C ↑y
m : M
n : N
⊢ C (↑(FreeAddMonoid.of (m, n)) + ↑y)
exact Cp _ _ (C1 ..) ih